1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro
5
6 Measurable spaces -- σ-algberas
7 -/
8 import data.set.disjointed order.galois_connection data.set.countable
src └─────────────────┘ └─────────────────────┘ └────────────────┘
9
10 /-!
11 # Measurable spaces and measurable functions
12
13 This file defines measurable spaces and the functions and isomorphisms
14 between them.
15
16 A measurable space is a set equipped with a σ-algebra, a collection of
17 subsets closed under complementation and countable union. A function
18 between measurable spaces is measurable if the preimage of each
19 measurable subset is measurable.
20
21 σ-algebras on a fixed set α form a complete lattice. Here we order
22 σ-algebras by writing m₁ ≤ m₂ if every set which is m₁-measurable is
23 also m₂-measurable (that is, m₁ is a subset of m₂). In particular, any
24 collection of subsets of α generates a smallest σ-algebra which
25 contains all of them. A function f : α → β induces a Galois connection
26 between the lattices of σ-algebras on α and β.
27
28 A measurable equivalence between measurable spaces is an equivalence
29 which respects the σ-algebras, that is, for which both directions of
30 the equivalence are measurable functions.
31
32 ## Main statements
33
34 The main theorem of this file is Dynkin's π-λ theorem, which appears
35 here as an induction principle `induction_on_inter`. Suppose s is a
36 collection of subsets of α such that the intersection of two members
37 of s belongs to s whenever it is nonempty. Let m be the σ-algebra
38 generated by s. In order to check that a predicate C holds on every
39 member of m, it suffices to check that C holds on the members of s and
40 that C is preserved by complementation and *disjoint* countable
41 unions.
42
43 ## Implementation notes
44
45 Measurability of a function f : α → β between measurable spaces is
46 defined in terms of the Galois connection induced by f.
47
48 ## References
49
50 * <https://en.wikipedia.org/wiki/Measurable_space>
51 * <https://en.wikipedia.org/wiki/Sigma-algebra>
52 * <https://en.wikipedia.org/wiki/Dynkin_system>
53
54 ## Tags
55
56 measurable space, measurable function, dynkin system
57 -/
58
59 local attribute [instance] classical.prop_decidable
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
60 open set lattice encodable
61 open_locale classical
62
63 universes u v w x
64 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort x}
id ┴
typ ┴
65 {s t u : set α}
id └─┘
src └─┘
typ └─┘
66
67 structure measurable_space (α : Type u) :=
id └──┘
typ └──┘
68 (is_measurable : set α → Prop)
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
69 (is_measurable_empty : is_measurable ∅)
id └───────────┘ ┴
src ┴
typ └───────────┘ ┴
70 (is_measurable_compl : ∀s, is_measurable s → is_measurable (- s))
id ┴ └───────────┘ ┴ └───────────┘ ┴ ┴
src ┴
typ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴
71 (is_measurable_Union : ∀f:ℕ → set α, (∀i, is_measurable (f i)) → is_measurable (⋃i, f i))
id ┴ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴┴┴ ┴ ┴
src ┴ └─┘ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴┴┴ ┴ ┴
doc ┴ ┴
72
73 attribute [class] measurable_space
id └──────────────┘
src └──────────────┘
typ └──────────────┘
74
75 section
76 variable [measurable_space α]
id └──────────────┘
src └──────────────┘
typ └──────────────┘
77
78 /-- `is_measurable s` means that `s` is measurable (in the ambient measure space on `α`) -/
79 def is_measurable : set α → Prop := ‹measurable_space α›.is_measurable
id └─┘ ┴ ┴└──────────────┘ ┴┴└───────────┘
src └─┘ ┴└──────────────┘ ┴└───────────┘
typ └─┘ ┴ ┴└──────────────┘ ┴┴└───────────┘
doc ┴ ┴
80
81 lemma is_measurable.empty : is_measurable (∅ : set α) :=
id └───────────┘ ┴ └─┘ ┴
src └───────────┘ ┴ └─┘
typ └───────────┘ ┴ └─┘ ┴
doc └───────────┘
82 ‹measurable_space α›.is_measurable_empty
id ┴└──────────────┘ ┴┴└─────────────────┘
src ┴└──────────────┘ ┴└─────────────────┘
typ ┴└──────────────┘ ┴┴└─────────────────┘
doc ┴ ┴
83
84 lemma is_measurable.compl : is_measurable s → is_measurable (-s) :=
id └───────────┘ ┴ └───────────┘ ┴┴
src └───────────┘ └───────────┘ ┴
typ └───────────┘ ┴ └───────────┘ ┴┴
doc └───────────┘ └───────────┘
85 ‹measurable_space α›.is_measurable_compl s
id ┴└──────────────┘ ┴┴└─────────────────┘ ┴
src ┴└──────────────┘ ┴└─────────────────┘
typ ┴└──────────────┘ ┴┴└─────────────────┘ ┴
doc ┴ ┴
86
87 lemma is_measurable.compl_iff : is_measurable (-s) ↔ is_measurable s :=
id └───────────┘ ┴┴ ┴ └───────────┘ ┴
src └───────────┘ ┴ ┴ └───────────┘
typ └───────────┘ ┴┴ ┴ └───────────┘ ┴
doc └───────────┘ └───────────┘
88 ⟨λ h, by simpa using h.compl, is_measurable.compl⟩
id ┴ └─────┘ └─────────────────┘
src └──────────┘└─────┘ └─────────────────┘
typ ┴ └──────────┘└─────┘ └─────────────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └──────────────────┘
89
90 lemma is_measurable.univ : is_measurable (univ : set α) :=
id └───────────┘ └──┘ └─┘ ┴
src └───────────┘ └──┘ └─┘
typ └───────────┘ └──┘ └─┘ ┴
doc └───────────┘
91 by simpa using (@is_measurable.empty α _).compl
id └─────────────────┘ ┴
src └──────────┘ └─────────────────┘┴ └─────────
typ └──────────┘ └─────────────────┘┴┴└─────────
doc └──────────┘ ┴ └─────────
txt └──────────┘ ┴ └─────────
par └──────────┘ ┴ └─────────
pid ┴└────┘ ┴ └──────┘└─
st └─────────────────────────────────────────────
92
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
93 lemma encodable.Union_decode2 {α} [encodable β] (f : β → set α) :
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
94 (⋃ b, f b) = ⋃ (i : ℕ) (b ∈ decode2 β i), f b :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
95 ext $ by simp [mem_decode2, exists_swap]
id └─┘ └─────────┘ └─────────┘
src └─┘ └────┘└─────────┘└┘└─────────┘└─
typ └─┘ └────┘└─────────┘└┘└─────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────────
96
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
97 @[elab_as_eliminator] lemma encodable.Union_decode2_cases
doc └────────────────┘
98 {α} [encodable β] {f : β → set α} {C : set α → Prop}
id └───────┘ ┴ ┴ └─┘ ┴ └─┘ ┴
src └───────┘ └─┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴ └─┘ ┴
doc └───────┘
99 (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
100 C (⋃ b ∈ decode2 β n, f b) :=
id ┴ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴
doc ┴ ┴
101 match decode2 β n with
id └─────┘ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴
102 | none := by simp; apply H0
id └──┘
src └──┘ └──┘ └────┘ ┴
typ └──┘ └──┘ └────┘ ┴
doc └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid ┴ ┴
st └──────────────┘
103 | (some b) := by convert H1 b; simp [ext_iff]
id └──┘ └┘ ┴ └─────┘
src └──┘ └──────┘ ┴ └────┘└─────┘└┘
typ └──┘ └──────┘└┘┴┴ └────┘└─────┘└┘
doc └──────┘ ┴ └────┘ └┘
txt └──────┘ ┴ └────┘ └┘
par └──────┘ ┴ └────┘ └┘
pid ┴ ┴ ┴┴ ┴┴
st └────────────────────────────┘
104 end
105
106 lemma is_measurable.Union [encodable β] {f : β → set α} (h : ∀b, is_measurable (f b)) :
id └───────┘ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src └───────┘ └─┘ └───────────┘
typ └───────┘ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────┘ └───────────┘
107 is_measurable (⋃b, f b) :=
id └───────────┘ ┴┴┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴┴┴ ┴ ┴
doc └───────────┘ ┴ ┴
108 by rw encodable.Union_decode2; exact
id └─────────────────────┘
src └─┘└─────────────────────┘ └────┘
typ └─┘└─────────────────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └──────────────────────────────────
109 ‹measurable_space α›.is_measurable_Union
id ┴└──────────────┘ ┴┴
src ┴└──────────────┘┴ ┴└────────────────────
typ ┴└──────────────┘┴┴┴└────────────────────
doc ┴ ┴ ┴└────────────────────
txt ┴ └────────────────────
par ┴ └────────────────────
pid ┴ └────────────────────
st ─────────────────────────────────────────
110 (λ n, ⋃ b ∈ decode2 β n, f b)
id ┴ └─────┘ ┴ ┴ ┴
src ─┘ └──┘┴└───┘└─────┘┴ ┴ ┴┴ ┴ └─
typ ─┘ └──┘┴└───┘└─────┘┴┴┴ ┴┴┴┴ └─
doc ─┘ └──┘┴└───┘ ┴ ┴ ┴┴ ┴ └─
txt ─┘ └──┘ └───┘ ┴ ┴ ┴ ┴ └─
par ─┘ └──┘ └───┘ ┴ ┴ ┴ ┴ └─
pid ─┘ └──┘ └───┘ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────
111 (λ n, encodable.Union_decode2_cases is_measurable.empty h)
id └───────────────────────────┘ └─────────────────┘ ┴
src ─┘ └──┘└───────────────────────────┘┴└─────────────────┘┴ └─
typ ─┘ └──┘└───────────────────────────┘┴└─────────────────┘┴┴└─
doc ─┘ └──┘ ┴ ┴ └─
txt ─┘ └──┘ ┴ ┴ └─
par ─┘ └──┘ ┴ ┴ └─
pid ─┘ └──┘ ┴ ┴ ┴└
st ─────────────────────────────────────────────────────────────
112
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
113 lemma is_measurable.bUnion {f : β → set α} {s : set β} (hs : countable s)
id ┴ └─┘ ┴ └─┘ ┴ └───────┘ ┴
src └─┘ └─┘ └───────┘
typ ┴ └─┘ ┴ └─┘ ┴ └───────┘ ┴
doc └───────┘
114 (h : ∀b∈s, is_measurable (f b)) : is_measurable (⋃b∈s, f b) :=
id ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴┴ ┴┴ ┴ ┴
src ┴ └───────────┘ └───────────┘ ┴ ┴
typ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴┴ ┴┴ ┴ ┴
doc └───────────┘ └───────────┘ ┴ ┴
115 begin
st └─────
116 rw bUnion_eq_Union,
id └─────────────┘
src └─┘└─────────────┘
typ └─┘└─────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────┘└─
117 haveI := hs.to_encodable,
id └─────────────┘
src └───────┘└─────────────┘
typ └───────┘└─────────────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└─┘
st ─────────────────────────┘└─
118 exact is_measurable.Union (by simpa using h)
id └─────────────────┘ ┴
src └────┘└─────────────────┘┴ ┴└──────────┘ └┘
typ └────┘└─────────────────┘┴ ┴└──────────┘┴└┘
doc └────┘ ┴ ┴└──────────┘ └┘
txt └────┘ ┴ ┴└──────────┘ └┘
par └────┘ ┴ ┴└──────────┘ └┘
pid ┴ ┴ └───────────┘ ┴┴
st ──────────────────────────────┘└────────────┘└┘
119 end
st └─┘
120
121 lemma is_measurable.sUnion {s : set (set α)} (hs : countable s) (h : ∀t∈s, is_measurable t) :
id └─┘ └─┘ ┴ └───────┘ ┴ ┴ ┴ └───────────┘ ┴
src └─┘ └─┘ └───────┘ └───────────┘
typ └─┘ └─┘ ┴ └───────┘ ┴ ┴ ┴ └───────────┘ ┴
doc └───────┘ └───────────┘
122 is_measurable (⋃₀ s) :=
id └───────────┘ └┘ ┴
src └───────────┘ └┘
typ └───────────┘ └┘ ┴
doc └───────────┘
123 by rw sUnion_eq_bUnion; exact is_measurable.bUnion hs h
id └──────────────┘ └──────────────────┘ └┘ ┴
src └─┘└──────────────┘ └────┘└──────────────────┘┴ ┴ └
typ └─┘└──────────────┘ └────┘└──────────────────┘┴└┘┴┴└
doc └─┘ └────┘ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────────
124
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
125 lemma is_measurable.Union_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
id ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src └─┘ └───────────┘
typ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
126 is_measurable (⋃b, f b) :=
id └───────────┘ ┴┴┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴┴┴ ┴ ┴
doc └───────────┘ ┴ ┴
127 by by_cases p; simp [h, hf, is_measurable.empty]
id ┴ ┴ └┘ └─────────────────┘
src └───────┘ └────┘ └┘ └┘└─────────────────┘└─
typ └───────┘┴ └────┘┴└┘└┘└┘└─────────────────┘└─
doc └───────┘ └────┘ └┘ └┘ └─
txt └───────┘ └────┘ └┘ └┘ └─
par └───────┘ └────┘ └┘ └┘ └─
pid ┴ ┴┴ └┘ └┘ ┴└
st └──────────────────────────────────────────────
128
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
129 lemma is_measurable.Inter [encodable β] {f : β → set α} (h : ∀b, is_measurable (f b)) :
id └───────┘ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src └───────┘ └─┘ └───────────┘
typ └───────┘ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────┘ └───────────┘
130 is_measurable (⋂b, f b) :=
id └───────────┘ ┴┴┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴┴┴ ┴ ┴
doc └───────────┘ ┴ ┴
131 is_measurable.compl_iff.1 $
id └─────────────────────┘┴
src └─────────────────────┘┴
typ └─────────────────────┘┴
132 by rw compl_Inter; exact is_measurable.Union (λ b, (h b).compl)
id └─────────┘ └─────────────────┘ ┴
src └─┘└─────────┘ └────┘└─────────────────┘┴ └──┘ ┴ └────────
typ └─┘└─────────┘ └────┘└─────────────────┘┴ └──┘ ┴┴ └────────
doc └─┘ └────┘ ┴ └──┘ ┴ └────────
txt └─┘ └────┘ ┴ └──┘ ┴ └────────
par └─┘ └────┘ ┴ └──┘ ┴ └────────
pid ┴ ┴ ┴ └──┘ ┴ └──────┘└
st └─────────────────────────────────────────────────────────────
133
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
134 lemma is_measurable.bInter {f : β → set α} {s : set β} (hs : countable s)
id ┴ └─┘ ┴ └─┘ ┴ └───────┘ ┴
src └─┘ └─┘ └───────┘
typ ┴ └─┘ ┴ └─┘ ┴ └───────┘ ┴
doc └───────┘
135 (h : ∀b∈s, is_measurable (f b)) : is_measurable (⋂b∈s, f b) :=
id ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴┴ ┴┴ ┴ ┴
src └───────────┘ └───────────┘ ┴ ┴
typ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴┴ ┴┴ ┴ ┴
doc └───────────┘ └───────────┘ ┴ ┴
136 is_measurable.compl_iff.1 $
id └─────────────────────┘┴
src └─────────────────────┘┴
typ └─────────────────────┘┴
137 by rw compl_bInter; exact is_measurable.bUnion hs (λ b hb, (h b hb).compl)
id └──────────┘ └──────────────────┘ └┘ ┴
src └─┘└──────────┘ └────┘└──────────────────┘┴ ┴ └─────┘ ┴ ┴ └────────
typ └─┘└──────────┘ └────┘└──────────────────┘┴└┘┴ └─────┘ ┴┴ ┴ └────────
doc └─┘ └────┘ ┴ ┴ └─────┘ ┴ ┴ └────────
txt └─┘ └────┘ ┴ ┴ └─────┘ ┴ ┴ └────────
par └─┘ └────┘ ┴ ┴ └─────┘ ┴ ┴ └────────
pid ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └──────┘└
st └────────────────────────────────────────────────────────────────────────
138
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
139 lemma is_measurable.sInter {s : set (set α)} (hs : countable s) (h : ∀t∈s, is_measurable t) :
id └─┘ └─┘ ┴ └───────┘ ┴ ┴ ┴ └───────────┘ ┴
src └─┘ └─┘ └───────┘ └───────────┘
typ └─┘ └─┘ ┴ └───────┘ ┴ ┴ ┴ └───────────┘ ┴
doc └───────┘ └───────────┘
140 is_measurable (⋂₀ s) :=
id └───────────┘ └┘ ┴
src └───────────┘ └┘
typ └───────────┘ └┘ ┴
doc └───────────┘ └┘
141 by rw sInter_eq_bInter; exact is_measurable.bInter hs h
id └──────────────┘ └──────────────────┘ └┘ ┴
src └─┘└──────────────┘ └────┘└──────────────────┘┴ ┴ └
typ └─┘└──────────────┘ └────┘└──────────────────┘┴└┘┴┴└
doc └─┘ └────┘ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────────
142
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
143 lemma is_measurable.Inter_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
id ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src └─┘ └───────────┘
typ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
144 is_measurable (⋂b, f b) :=
id └───────────┘ ┴┴┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴┴┴ ┴ ┴
doc └───────────┘ ┴ ┴
145 by by_cases p; simp [h, hf, is_measurable.univ]
id ┴ ┴ └┘ └────────────────┘
src └───────┘ └────┘ └┘ └┘└────────────────┘└─
typ └───────┘┴ └────┘┴└┘└┘└┘└────────────────┘└─
doc └───────┘ └────┘ └┘ └┘ └─
txt └───────┘ └────┘ └┘ └┘ └─
par └───────┘ └────┘ └┘ └┘ └─
pid ┴ ┴┴ └┘ └┘ ┴└
st └─────────────────────────────────────────────
146
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
147 lemma is_measurable.union {s₁ s₂ : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
148 (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ ∪ s₂) :=
id └───────────┘ └┘ └───────────┘ └┘ └───────────┘ └┘ ┴ └┘
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ └┘ └───────────┘ └┘ └───────────┘ └┘ ┴ └┘
doc └───────────┘ └───────────┘ └───────────┘
149 by rw union_eq_Union; exact
id └────────────┘
src └─┘└────────────┘ └────┘
typ └─┘└────────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └─────────────────────────
150 is_measurable.Union (bool.forall_bool.2 ⟨h₂, h₁⟩)
id └─────────────────┘ └──────────────┘ └┘ └┘
src └─────────────────┘┴ └──────────────┘└─┘ └┘ └──
typ └─────────────────┘┴ └──────────────┘└─┘ └┘└┘└┘└──
doc ┴ └─┘ └┘ └──
txt ┴ └─┘ └┘ └──
par ┴ └─┘ └┘ └──
pid ┴ └─┘ └┘ └┘└
st ──────────────────────────────────────────────────
151
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
152 lemma is_measurable.inter {s₁ s₂ : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
153 (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ ∩ s₂) :=
id └───────────┘ └┘ └───────────┘ └┘ └───────────┘ └┘ ┴ └┘
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ └┘ └───────────┘ └┘ └───────────┘ └┘ ┴ └┘
doc └───────────┘ └───────────┘ └───────────┘
154 by rw inter_eq_compl_compl_union_compl; exact
id └──────────────────────────────┘
src └─┘└──────────────────────────────┘ └────┘
typ └─┘└──────────────────────────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └───────────────────────────────────────────
155 (h₁.compl.union h₂.compl).compl
id └────────────┘ └──────┘
src └────────────┘┴└──────┘└───────
typ └────────────┘┴└──────┘└───────
doc ┴ └───────
txt ┴ └───────
par ┴ └───────
pid ┴ └────┘└─
st ────────────────────────────────
156
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
157 lemma is_measurable.diff {s₁ s₂ : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
158 (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ \ s₂) :=
id └───────────┘ └┘ └───────────┘ └┘ └───────────┘ └┘ ┴ └┘
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ └┘ └───────────┘ └┘ └───────────┘ └┘ ┴ └┘
doc └───────────┘ └───────────┘ └───────────┘
159 h₁.inter h₂.compl
id └┘└────┘ └┘└────┘
src └────┘ └────┘
typ └┘└────┘ └┘└────┘
160
161 lemma is_measurable.sub {s₁ s₂ : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
162 is_measurable s₁ → is_measurable s₂ → is_measurable (s₁ - s₂) :=
id └───────────┘ └┘ └───────────┘ └┘ └───────────┘ └┘ ┴ └┘
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ └┘ └───────────┘ └┘ └───────────┘ └┘ ┴ └┘
doc └───────────┘ └───────────┘ └───────────┘
163 is_measurable.diff
id └────────────────┘
src └────────────────┘
typ └────────────────┘
164
165 lemma is_measurable.disjointed {f : ℕ → set α} (h : ∀i, is_measurable (f i)) (n) :
id ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src ┴ └─┘ └───────────┘
typ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
166 is_measurable (disjointed f n) :=
id └───────────┘ └────────┘ ┴ ┴
src └───────────┘ └────────┘
typ └───────────┘ └────────┘ ┴ ┴
doc └───────────┘ └────────┘
167 disjointed_induct (h n) (assume t i ht, is_measurable.diff ht $ h _)
id └───────────────┘ ┴ ┴ ┴ ┴ └┘ └────────────────┘ └┘ ┴
src └───────────────┘ └────────────────┘
typ └───────────────┘ ┴ ┴ ┴ ┴ └┘ └────────────────┘ └┘ ┴
168
169 lemma is_measurable.const (p : Prop) : is_measurable {a : α | p} :=
id └───────────┘ ┴ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴ ┴
doc └───────────┘
170 by by_cases p; simp [h, is_measurable.empty]; apply is_measurable.univ
id ┴ ┴ └─────────────────┘ └────────────────┘
src └───────┘ └────┘ └┘└─────────────────┘┴ └────┘└────────────────┘└
typ └───────┘┴ └────┘┴└┘└─────────────────┘┴ └────┘└────────────────┘└
doc └───────┘ └────┘ └┘ ┴ └────┘ └
txt └───────┘ └────┘ └┘ ┴ └────┘ └
par └───────┘ └────┘ └┘ ┴ └────┘ └
pid ┴ ┴┴ └┘ ┴ ┴ └
st └────────────────────────────────────────────────────────────────────
171
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
172 end
173
174 @[ext] lemma measurable_space.ext :
doc └─┘
175 ∀{m₁ m₂ : measurable_space α}, (∀s:set α, m₁.is_measurable s ↔ m₂.is_measurable s) → m₁ = m₂
id ┴ └──────────────┘ ┴ ┴ └─┘ ┴ └┘└────────────┘ ┴ ┴ └┘└────────────┘ ┴ └┘ ┴ └┘
src └──────────────┘ └─┘ └────────────┘ ┴ └────────────┘ ┴
typ ┴ └──────────────┘ ┴ ┴ └─┘ ┴ └┘└────────────┘ ┴ ┴ └┘└────────────┘ ┴ └┘ ┴ └┘
176 | ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h :=
id └┘ └┘ ┴
typ └┘ └┘ ┴
177 have s₁ = s₂, from funext $ assume x, propext $ h x,
id ┴ └────┘ ┴ └─────┘ ┴
src ┴ └────┘ └─────┘
typ ┴ └────┘ ┴ └─────┘ ┴
178 by subst this
id └──┘
src └────┘ └
typ └────┘└──┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st └───────────
179
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
180 namespace measurable_space
181
182 section complete_lattice
183
184 instance : partial_order (measurable_space α) :=
id └───────────┘ └──────────────┘ ┴
src └───────────┘ └──────────────┘
typ └───────────┘ └──────────────┘ ┴
185 { le := λm₁ m₂, m₁.is_measurable ≤ m₂.is_measurable,
id ┴ └┘ └┘ └┘└────────────┘ ┴ └┘└────────────┘
src ┴ └────────────┘ ┴ └────────────┘
typ ┴ └┘ └┘ └┘└────────────┘ ┴ └┘└────────────┘
186 le_refl := assume a b, le_refl _,
id ┴ ┴ └─────┘
src └─────┘
typ ┴ ┴ └─────┘
187 le_trans := assume a b c, le_trans,
id ┴ ┴ ┴ └──────┘
src └──────┘
typ ┴ ┴ ┴ └──────┘
188 le_antisymm := assume a b h₁ h₂, measurable_space.ext $ assume s, ⟨h₁ s, h₂ s⟩ }
id ┴ ┴ └┘ └┘ └──────────────────┘ ┴ └┘ ┴ └┘ ┴
src └──────────────────┘
typ ┴ ┴ └┘ └┘ └──────────────────┘ ┴ └┘ ┴ └┘ ┴
189
190 /-- The smallest σ-algebra containing a collection `s` of basic sets -/
191 inductive generate_measurable (s : set (set α)) : set α → Prop
id └─┘ └─┘ ┴ └─┘
src └─┘ └─┘ └─┘
typ └─┘ └─┘ ┴ └─┘
192 | basic : ∀u∈s, generate_measurable u
id ┴ ┴
typ ┴ ┴
193 | empty : generate_measurable ∅
id ┴
src ┴
typ ┴
194 | compl : ∀s, generate_measurable s → generate_measurable (-s)
id ┴ └─────────────────┘ ┴ ┴┴
src ┴
typ ┴ └─────────────────┘ ┴ ┴┴
195 | union : ∀f:ℕ → set α, (∀n, generate_measurable (f n)) → generate_measurable (⋃i, f i)
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴
196
197 /-- Construct the smallest measure space containing a collection of basic sets -/
198 def generate_from (s : set (set α)) : measurable_space α :=
id └─┘ └─┘ ┴ └──────────────┘ ┴
src └─┘ └─┘ └──────────────┘
typ └─┘ └─┘ ┴ └──────────────┘ ┴
199 { is_measurable := generate_measurable s,
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
doc └─────────────────┘
200 is_measurable_empty := generate_measurable.empty s,
id └───────────────────────┘ ┴
src └───────────────────────┘
typ └───────────────────────┘ ┴
201 is_measurable_compl := generate_measurable.compl,
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
202 is_measurable_Union := generate_measurable.union }
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
203
204 lemma is_measurable_generate_from {s : set (set α)} {t : set α} (ht : t ∈ s) :
id └─┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ └─┘ ┴
typ └─┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴
205 (generate_from s).is_measurable t :=
id └───────────┘ ┴ └───────────┘ ┴
src └───────────┘ └───────────┘
typ └───────────┘ ┴ └───────────┘ ┴
doc └───────────┘
206 generate_measurable.basic t ht
id └───────────────────────┘ ┴ └┘
src └───────────────────────┘
typ └───────────────────────┘ ┴ └┘
207
208 lemma generate_from_le {s : set (set α)} {m : measurable_space α} (h : ∀t∈s, m.is_measurable t) :
id └─┘ └─┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴└────────────┘ ┴
src └─┘ └─┘ └──────────────┘ └────────────┘
typ └─┘ └─┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴└────────────┘ ┴
209 generate_from s ≤ m :=
id └───────────┘ ┴ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴ ┴
doc └───────────┘
210 assume t (ht : generate_measurable s t), ht.rec_on h
id ┴ └─────────────────┘ ┴ ┴ └┘└─────┘ ┴
src └─────────────────┘ └─────┘
typ ┴ └─────────────────┘ ┴ ┴ └┘└─────┘ ┴
doc └─────────────────┘
211 (is_measurable_empty m)
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
212 (assume s _ hs, is_measurable_compl m s hs)
id ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └┘
src └─────────────────┘
typ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └┘
213 (assume f _ hf, is_measurable_Union m f hf)
id ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └┘
src └─────────────────┘
typ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └┘
214
215 lemma generate_from_le_iff {s : set (set α)} {m : measurable_space α} :
id └─┘ └─┘ ┴ └──────────────┘ ┴
src └─┘ └─┘ └──────────────┘
typ └─┘ └─┘ ┴ └──────────────┘ ┴
216 generate_from s ≤ m ↔ s ⊆ {t | m.is_measurable t} :=
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴└────────────┘ ┴
src └───────────┘ ┴ ┴ ┴ ┴ └────────────┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴└────────────┘ ┴
doc └───────────┘
217 iff.intro
id └───────┘
src └───────┘
typ └───────┘
218 (assume h u hu, h _ $ is_measurable_generate_from hu)
id ┴ ┴ └┘ ┴ └─────────────────────────┘ └┘
src └─────────────────────────┘
typ ┴ ┴ └┘ ┴ └─────────────────────────┘ └┘
219 (assume h, generate_from_le h)
id ┴ └──────────────┘ ┴
src └──────────────┘
typ ┴ └──────────────┘ ┴
220
221 protected def mk_of_closure (g : set (set α)) (hg : {t | (generate_from g).is_measurable t} = g) :
id └─┘ └─┘ ┴ ┴┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └─┘ └─┘ ┴ └───────────┘ └───────────┘ ┴
typ └─┘ └─┘ ┴ ┴┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘
222 measurable_space α :=
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
223 { is_measurable := λs, s ∈ g,
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
224 is_measurable_empty := hg ▸ is_measurable_empty _,
id └┘ ┴ └─────────────────┘
src ┴ └─────────────────┘
typ └┘ ┴ └─────────────────┘
225 is_measurable_compl := hg ▸ is_measurable_compl _,
id └┘ ┴ └─────────────────┘
src ┴ └─────────────────┘
typ └┘ ┴ └─────────────────┘
226 is_measurable_Union := hg ▸ is_measurable_Union _ }
id └┘ ┴ └─────────────────┘
src ┴ └─────────────────┘
typ └┘ ┴ └─────────────────┘
227
228 lemma mk_of_closure_sets {s : set (set α)}
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
229 {hs : {t | (generate_from s).is_measurable t} = s} :
id ┴┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
src ┴ └───────────┘ └───────────┘ ┴
typ ┴┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘
230 measurable_space.mk_of_closure s hs = generate_from s :=
id └────────────────────────────┘ ┴ └┘ ┴ └───────────┘ ┴
src └────────────────────────────┘ ┴ └───────────┘
typ └────────────────────────────┘ ┴ └┘ ┴ └───────────┘ ┴
doc └───────────┘
231 measurable_space.ext $ assume t, show t ∈ s ↔ _, by rw [← hs] {occs := occurrences.pos [1] }; refl
id └──────────────────┘ ┴ ┴ ┴ ┴ ┴ └┘ └─────────────┘ ┴ ┴
src └──────────────────┘ ┴ ┴ └────┘ └┘ └──────┘└─────────────┘┴┴┴┴└┘ └────
typ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ └────┘└┘└┘ └──────┘└─────────────┘┴┴┴┴└┘ └────
doc └────┘ └┘ └──────┘ ┴ ┴ └┘ └────
txt └────┘ └┘ └──────┘ ┴ ┴ └┘ └────
par └────┘ └┘ └──────┘ ┴ ┴ └┘ └────
pid └──┘ ┴┴ └──────┘ ┴ ┴ └┘ └
st └───────┘┴└─────────────────────────────────────
232
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
233 def gi_generate_from : galois_insertion (@generate_from α) (λm, {t | @is_measurable α m t}) :=
id └──────────────┘ └───────────┘ ┴ ┴ ┴┴ └───────────┘ ┴ ┴ ┴
src └──────────────┘ └───────────┘ ┴ └───────────┘
typ └──────────────┘ └───────────┘ ┴ ┴ ┴┴ └───────────┘ ┴ ┴ ┴
doc └──────────────┘ └───────────┘
234 { gc := assume s m, generate_from_le_iff,
id ┴ ┴ └──────────────────┘
src └──────────────────┘
typ ┴ ┴ └──────────────────┘
235 le_l_u := assume m s, is_measurable_generate_from,
id ┴ ┴ └─────────────────────────┘
src └─────────────────────────┘
typ ┴ ┴ └─────────────────────────┘
236 choice :=
237 λg hg, measurable_space.mk_of_closure g $ le_antisymm hg $ generate_from_le_iff.1 $ le_refl _,
id ┴ └┘ └────────────────────────────┘ ┴ └─────────┘ └┘ └──────────────────┘┴ └─────┘
src └────────────────────────────┘ └─────────┘ └──────────────────┘┴ └─────┘
typ ┴ └┘ └────────────────────────────┘ ┴ └─────────┘ └┘ └──────────────────┘┴ └─────┘
238 choice_eq := assume g hg, mk_of_closure_sets }
id ┴ └┘ └────────────────┘
src └────────────────┘
typ ┴ └┘ └────────────────┘
239
240 instance : complete_lattice (measurable_space α) :=
id └──────────────┘ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ └──────────────┘ ┴
doc └──────────────┘
241 gi_generate_from.lift_complete_lattice
id └──────────────┘└────────────────────┘
src └──────────────┘└────────────────────┘
typ └──────────────┘└────────────────────┘
doc └────────────────────┘
242
243 instance : inhabited (measurable_space α) := ⟨⊤⟩
id └───────┘ └──────────────┘ ┴ ┴
src └───────┘ └──────────────┘ ┴
typ └───────┘ └──────────────┘ ┴ ┴
244
245 lemma is_measurable_bot_iff {s : set α} : @is_measurable α ⊥ s ↔ (s = ∅ ∨ s = univ) :=
id └─┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └─┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ └─┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
246 let b : measurable_space α :=
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
247 { is_measurable := λs, s = ∅ ∨ s = univ,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
248 is_measurable_empty := or.inl rfl,
id └────┘ └─┘
src └────┘ └─┘
typ └────┘ └─┘
249 is_measurable_compl := by simp [or_imp_distrib] {contextual := tt},
id └────────────┘ └┘
src └────┘└────────────┘└┘ └────────────┘└┘┴
typ └────┘└────────────┘└┘ └────────────┘└┘┴
doc └────┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └────────────┘ ┴
par └────┘ └┘ └────────────┘ ┴
pid ┴┴ ┴┴ └────────────┘ ┴
st └───────────────────────────────────────┘
250 is_measurable_Union := assume f hf, classical.by_cases
id ┴ └┘ └────────────────┘
src └────────────────┘
typ ┴ └┘ └────────────────┘
251 (assume h : ∃i, f i = univ,
id ┴┴┴ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ └──┘
typ ┴┴┴ ┴ ┴ ┴ └──┘
252 let ⟨i, hi⟩ := h in
id └─┘ ┴ └┘ ┴
typ └─┘ ┴ └┘ ┴
253 or.inr $ eq_univ_of_univ_subset $ hi ▸ le_supr f i)
id └────┘ └────────────────────┘ ┴ └─────┘ ┴
src └────┘ └────────────────────┘ ┴ └─────┘
typ └────┘ └────────────────────┘ ┴ └─────┘ ┴
254 (assume h : ¬ ∃i, f i = univ,
id ┴ ┴┴┴ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴┴┴ ┴ ┴ ┴ └──┘
255 or.inl $ eq_empty_of_subset_empty $ Union_subset $ assume i,
id └────┘ └──────────────────────┘ └──────────┘ ┴
src └────┘ └──────────────────────┘ └──────────┘
typ └────┘ └──────────────────────┘ └──────────┘ ┴
256 (hf i).elim (by simp {contextual := tt}) (assume hi, false.elim $ h ⟨i, hi⟩)) } in
id └┘ ┴ └──┘ └┘ └┘ └────────┘ ┴ ┴ └┘
src └──┘ └───┘ └────────────┘└┘┴ └────────┘
typ └┘ ┴ └──┘ └───┘ └────────────┘└┘┴ └┘ └────────┘ ┴ ┴ └┘
doc └───┘ └────────────┘ ┴
txt └───┘ └────────────┘ ┴
par └───┘ └────────────┘ ┴
pid ┴ └────────────┘ ┴
st └──────────────────────┘
257 have b = ⊥, from bot_unique $ assume s hs,
id ┴ ┴ ┴ └────────┘ ┴ └┘
src ┴ ┴ └────────┘
typ ┴ ┴ ┴ └────────┘ ┴ └┘
258 hs.elim (assume s, s.symm ▸ @is_measurable_empty _ ⊥) (assume s, s.symm ▸ @is_measurable.univ _ ⊥),
id └┘└───┘ ┴ ┴└───┘ ┴ └─────────────────┘ ┴ ┴ ┴└───┘ ┴ └────────────────┘ ┴
src └───┘ └───┘ ┴ └─────────────────┘ ┴ └───┘ ┴ └────────────────┘ ┴
typ └┘└───┘ ┴ ┴└───┘ ┴ └─────────────────┘ ┴ ┴ ┴└───┘ ┴ └────────────────┘ ┴
259 this ▸ iff.rfl
id └──┘ ┴ └─────┘
src ┴ └─────┘
typ └──┘ ┴ └─────┘
260
261 @[simp] theorem is_measurable_top {s : set α} : @is_measurable _ ⊤ s := trivial
id └─┘ ┴ └───────────┘ ┴ ┴ └─────┘
src └─┘ └───────────┘ ┴ └─────┘
typ └─┘ ┴ └───────────┘ ┴ ┴ └─────┘
doc └──┘
262
263 @[simp] theorem is_measurable_inf {m₁ m₂ : measurable_space α} {s : set α} :
id └──────────────┘ ┴ └─┘ ┴
src └──────────────┘ └─┘
typ └──────────────┘ ┴ └─┘ ┴
doc └──┘
264 @is_measurable _ (m₁ ⊓ m₂) s ↔ @is_measurable _ m₁ s ∧ @is_measurable _ m₂ s :=
id └───────────┘ └┘ ┴ └┘ ┴ ┴ └───────────┘ └┘ ┴ ┴ └───────────┘ └┘ ┴
src └───────────┘ ┴ ┴ └───────────┘ ┴ └───────────┘
typ └───────────┘ └┘ ┴ └┘ ┴ ┴ └───────────┘ └┘ ┴ ┴ └───────────┘ └┘ ┴
265 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
266
267 @[simp] theorem is_measurable_Inf {ms : set (measurable_space α)} {s : set α} :
id └─┘ └──────────────┘ ┴ └─┘ ┴
src └─┘ └──────────────┘ └─┘
typ └─┘ └──────────────┘ ┴ └─┘ ┴
doc └──┘
268 @is_measurable _ (Inf ms) s ↔ ∀ m ∈ ms, @is_measurable _ m s :=
id └───────────┘ └─┘ └┘ ┴ ┴ ┴ └┘ └───────────┘ ┴ ┴
src └───────────┘ └─┘ ┴ └───────────┘
typ └───────────┘ └─┘ └┘ ┴ ┴ ┴ └┘ └───────────┘ ┴ ┴
doc └─┘
269 show s ∈ (⋂m∈ms, {t | @is_measurable _ m t }) ↔ _, by simp
id ┴ ┴ ┴┴ └┘┴ ┴┴ └───────────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └───────────┘ ┴ └────
typ ┴ ┴ ┴┴ └┘┴ ┴┴ └───────────┘ ┴ ┴ ┴ └────
doc ┴ ┴ └────
txt └────
par └────
pid └
st └─────
270
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
271 @[simp] theorem is_measurable_infi {ι} {m : ι → measurable_space α} {s : set α} :
id ┴ └──────────────┘ ┴ └─┘ ┴
src └──────────────┘ └─┘
typ ┴ └──────────────┘ ┴ └─┘ ┴
doc └──┘
272 @is_measurable _ (infi m) s ↔ ∀ i, @is_measurable _ (m i) s :=
id └───────────┘ └──┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ └──┘ ┴ └───────────┘
typ └───────────┘ └──┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └──┘
273 show s ∈ (λm, {s | @is_measurable _ m s }) (infi m) ↔ _, by rw (@gi_generate_from α).gc.u_infi; simp; refl
id ┴ ┴ ┴ ┴┴ └───────────┘ ┴ ┴ └──┘ ┴ ┴ └──────────────┘ ┴
src ┴ ┴ └───────────┘ └──┘ ┴ └─┘ └──────────────┘┴ └─────────┘ └──┘ └────
typ ┴ ┴ ┴ ┴┴ └───────────┘ ┴ ┴ └──┘ ┴ ┴ └─┘ └──────────────┘┴┴└─────────┘ └──┘ └────
doc └──┘ └─┘ ┴ └─────────┘ └──┘ └────
txt └─┘ ┴ └─────────┘ └──┘ └────
par └─┘ ┴ └─────────┘ └──┘ └────
pid ┴ ┴ └────────┘┴ └
st └───────────────────────────────────────────────
274
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
275 end complete_lattice
276
277 section functors
278 variables {m m₁ m₂ : measurable_space α} {m' : measurable_space β} {f : α → β} {g : β → α}
id └──────────────┘ └──────────────┘
src └──────────────┘ └──────────────┘
typ └──────────────┘ └──────────────┘
279
280 /-- The forward image of a measure space under a function. `map f m` contains the sets `s : set β`
281 whose preimage under `f` is measurable. -/
282 protected def map (f : α → β) (m : measurable_space α) : measurable_space β :=
id ┴ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ ┴ ┴ └──────────────┘ ┴ └──────────────┘ ┴
283 { is_measurable := λs, m.is_measurable $ f ⁻¹' s,
id ┴ ┴└────────────┘ ┴ └─┘ ┴
src └────────────┘ └─┘
typ ┴ ┴└────────────┘ ┴ └─┘ ┴
doc └─┘
284 is_measurable_empty := m.is_measurable_empty,
id ┴└──────────────────┘
src └──────────────────┘
typ ┴└──────────────────┘
285 is_measurable_compl := assume s hs, m.is_measurable_compl _ hs,
id ┴ └┘ ┴└──────────────────┘ └┘
src └──────────────────┘
typ ┴ └┘ ┴└──────────────────┘ └┘
286 is_measurable_Union := assume f hf, by rw [preimage_Union]; exact m.is_measurable_Union _ hf }
id ┴ └┘ └────────────┘ └───────────────────┘ └┘
src └──┘└────────────┘┴ └────┘└───────────────────┘└─┘ ┴
typ ┴ └┘ └──┘└────────────┘┴ └────┘└───────────────────┘└─┘└┘┴
doc └──┘ ┴ └────┘ └─┘ ┴
txt └──┘ ┴ └────┘ └─┘ ┴
par └──┘ ┴ └────┘ └─┘ ┴
pid └┘ ┴ ┴ └─┘ ┴
st └─────────────────┘┴└─────────────────────────────────┘
287
288 @[simp] lemma map_id : m.map id = m :=
id ┴└──┘ └┘ ┴ ┴
src └──┘ └┘ ┴
typ ┴└──┘ └┘ ┴ ┴
doc └──┘ └──┘
289 measurable_space.ext $ assume s, iff.rfl
id └──────────────────┘ ┴ └─────┘
src └──────────────────┘ └─────┘
typ └──────────────────┘ ┴ └─────┘
290
291 @[simp] lemma map_comp {f : α → β} {g : β → γ} : (m.map f).map g = m.map (g ∘ f) :=
id ┴ ┴ ┴ ┴ ┴└──┘ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴
src └──┘ └─┘ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴└──┘ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴
doc └──┘ └──┘ └─┘ └──┘
292 measurable_space.ext $ assume s, iff.rfl
id └──────────────────┘ ┴ └─────┘
src └──────────────────┘ └─────┘
typ └──────────────────┘ ┴ └─────┘
293
294 /-- The reverse image of a measure space under a function. `comap f m` contains the sets `s : set α`
295 such that `s` is the `f`-preimage of a measurable set in `β`. -/
296 protected def comap (f : α → β) (m : measurable_space β) : measurable_space α :=
id ┴ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ ┴ ┴ └──────────────┘ ┴ └──────────────┘ ┴
297 { is_measurable := λs, ∃s', m.is_measurable s' ∧ f ⁻¹' s' = s,
id ┴ ┴└┘┴ ┴└────────────┘ └┘ ┴ ┴ └─┘ └┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴ └─┘ ┴
typ ┴ ┴└┘┴ ┴└────────────┘ └┘ ┴ ┴ └─┘ └┘ ┴ ┴
doc └─┘
298 is_measurable_empty := ⟨∅, m.is_measurable_empty, rfl⟩,
id ┴ ┴└──────────────────┘ └─┘
src ┴ └──────────────────┘ └─┘
typ ┴ ┴└──────────────────┘ └─┘
299 is_measurable_compl := assume s ⟨s', h₁, h₂⟩, ⟨-s', m.is_measurable_compl _ h₁, h₂ ▸ rfl⟩,
id ┴ ┴└┘ └┘ └┘ ┴ ┴└──────────────────┘ ┴ └─┘
src ┴ └──────────────────┘ ┴ └─┘
typ ┴ ┴└┘ └┘ └┘ ┴ ┴└──────────────────┘ ┴ └─┘
300 is_measurable_Union := assume s hs,
id ┴ └┘
typ ┴ └┘
301 let ⟨s', hs'⟩ := classical.axiom_of_choice hs in
id └─┘ └┘ └─┘ └───────────────────────┘ └┘
src └───────────────────────┘
typ └─┘ └┘ └─┘ └───────────────────────┘ └┘
302 ⟨⋃i, s' i, m.is_measurable_Union _ (λi, (hs' i).left), by simp [hs'] ⟩ }
id ┴┴┴ ┴ ┴└──────────────────┘ ┴ ┴ └──┘ └─┘
src ┴ ┴ └──────────────────┘ └──┘ └────┘ └┘
typ ┴┴┴ ┴ ┴└──────────────────┘ ┴ ┴ └──┘ └────┘└─┘└┘
doc ┴ ┴ └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └──────────┘
303
304 @[simp] lemma comap_id : m.comap id = m :=
id ┴└────┘ └┘ ┴ ┴
src └────┘ └┘ ┴
typ ┴└────┘ └┘ ┴ ┴
doc └──┘ └────┘
305 measurable_space.ext $ assume s, ⟨assume ⟨s', hs', h⟩, h ▸ hs', assume h, ⟨s, h, rfl⟩⟩
id └──────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └──────────────────┘ ┴ └─┘
typ └──────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘
306
307 @[simp] lemma comap_comp {f : β → α} {g : γ → β} : (m.comap f).comap g = m.comap (f ∘ g) :=
id ┴ ┴ ┴ ┴ ┴└────┘ ┴ └───┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴
src └────┘ └───┘ ┴ └────┘ ┴
typ ┴ ┴ ┴ ┴ ┴└────┘ ┴ └───┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴
doc └──┘ └────┘ └───┘ └────┘
308 measurable_space.ext $ assume s,
id └──────────────────┘ ┴
src └──────────────────┘
typ └──────────────────┘ ┴
309 ⟨assume ⟨t, ⟨u, h, hu⟩, ht⟩, ⟨u, h, ht ▸ hu ▸ rfl⟩, assume ⟨t, h, ht⟩, ⟨f ⁻¹' t, ⟨_, h, rfl⟩, ht⟩⟩
id ┴ ┴ ┴ └┘ └┘ ┴ ┴ └─┘ ┴┴ ┴ └┘ ┴ └─┘ └─┘
src ┴ ┴ └─┘ └─┘ └─┘
typ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └─┘ ┴┴ ┴ └┘ ┴ └─┘ └─┘
doc └─┘
310
311 lemma comap_le_iff_le_map {f : α → β} : m'.comap f ≤ m ↔ m' ≤ m.map f :=
id ┴ ┴ └┘└────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴└──┘ ┴
src └────┘ ┴ ┴ ┴ └──┘
typ ┴ ┴ └┘└────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴└──┘ ┴
doc └────┘ └──┘
312 ⟨assume h s hs, h _ ⟨_, hs, rfl⟩, assume h s ⟨t, ht, heq⟩, heq ▸ h _ ht⟩
id ┴ ┴ └┘ ┴ └┘ └─┘ ┴ ┴ ┴ └┘ └─┘ ┴ ┴
src └─┘ └─┘ ┴
typ ┴ ┴ └┘ ┴ └┘ └─┘ ┴ ┴ ┴ └┘ └─┘ ┴ ┴
313
314 lemma gc_comap_map (f : α → β) :
id ┴ ┴
typ ┴ ┴
315 galois_connection (measurable_space.comap f) (measurable_space.map f) :=
id └───────────────┘ └────────────────────┘ ┴ └──────────────────┘ ┴
src └───────────────┘ └────────────────────┘ └──────────────────┘
typ └───────────────┘ └────────────────────┘ ┴ └──────────────────┘ ┴
doc └───────────────┘ └────────────────────┘ └──────────────────┘
316 assume f g, comap_le_iff_le_map
id ┴ ┴ └─────────────────┘
src └─────────────────┘
typ ┴ ┴ └─────────────────┘
317
318 lemma map_mono (h : m₁ ≤ m₂) : m₁.map f ≤ m₂.map f := (gc_comap_map f).monotone_u h
id └┘ ┴ └┘ └┘└──┘ ┴ ┴ └┘└──┘ ┴ └──────────┘ ┴ └────────┘ ┴
src ┴ └──┘ ┴ └──┘ └──────────┘ └────────┘
typ └┘ ┴ └┘ └┘└──┘ ┴ ┴ └┘└──┘ ┴ └──────────┘ ┴ └────────┘ ┴
doc └──┘ └──┘
319 lemma monotone_map : monotone (measurable_space.map f) := assume a b h, map_mono h
id └──────┘ └──────────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └──────┘ └──────────────────┘ └──────┘
typ └──────┘ └──────────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────────────────┘
320 lemma comap_mono (h : m₁ ≤ m₂) : m₁.comap g ≤ m₂.comap g := (gc_comap_map g).monotone_l h
id └┘ ┴ └┘ └┘└────┘ ┴ ┴ └┘└────┘ ┴ └──────────┘ ┴ └────────┘ ┴
src ┴ └────┘ ┴ └────┘ └──────────┘ └────────┘
typ └┘ ┴ └┘ └┘└────┘ ┴ ┴ └┘└────┘ ┴ └──────────┘ ┴ └────────┘ ┴
doc └────┘ └────┘
321 lemma monotone_comap : monotone (measurable_space.comap g) := assume a b h, comap_mono h
id └──────┘ └────────────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
src └──────┘ └────────────────────┘ └────────┘
typ └──────┘ └────────────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └──────┘ └────────────────────┘
322
323 @[simp] lemma comap_bot : (⊥:measurable_space α).comap g = ⊥ := (gc_comap_map g).l_bot
id ┴ └──────────────┘ ┴ └───┘ ┴ ┴ ┴ └──────────┘ ┴ └───┘
src ┴ └──────────────┘ └───┘ ┴ ┴ └──────────┘ └───┘
typ ┴ └──────────────┘ ┴ └───┘ ┴ ┴ ┴ └──────────┘ ┴ └───┘
doc └──┘ └───┘
324 @[simp] lemma comap_sup : (m₁ ⊔ m₂).comap g = m₁.comap g ⊔ m₂.comap g := (gc_comap_map g).l_sup
id └┘ ┴ └┘ └───┘ ┴ ┴ └┘└────┘ ┴ ┴ └┘└────┘ ┴ └──────────┘ ┴ └───┘
src ┴ └───┘ ┴ └────┘ ┴ └────┘ └──────────┘ └───┘
typ └┘ ┴ └┘ └───┘ ┴ ┴ └┘└────┘ ┴ ┴ └┘└────┘ ┴ └──────────┘ ┴ └───┘
doc └──┘ └───┘ └────┘ └────┘
325 @[simp] lemma comap_supr {m : ι → measurable_space α} :(⨆i, m i).comap g = (⨆i, (m i).comap g) :=
id ┴ └──────────────┘ ┴ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴┴┴ ┴ ┴ └───┘ ┴
src └──────────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘
typ ┴ └──────────────┘ ┴ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴┴┴ ┴ ┴ └───┘ ┴
doc └──┘ ┴ ┴ └───┘ ┴ ┴ └───┘
326 (gc_comap_map g).l_supr
id └──────────┘ ┴ └────┘
src └──────────┘ └────┘
typ └──────────┘ ┴ └────┘
327
328 @[simp] lemma map_top : (⊤:measurable_space α).map f = ⊤ := (gc_comap_map f).u_top
id ┴ └──────────────┘ ┴ └─┘ ┴ ┴ ┴ └──────────┘ ┴ └───┘
src ┴ └──────────────┘ └─┘ ┴ ┴ └──────────┘ └───┘
typ ┴ └──────────────┘ ┴ └─┘ ┴ ┴ ┴ └──────────┘ ┴ └───┘
doc └──┘ └─┘
329 @[simp] lemma map_inf : (m₁ ⊓ m₂).map f = m₁.map f ⊓ m₂.map f := (gc_comap_map f).u_inf
id └┘ ┴ └┘ └─┘ ┴ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴ └──────────┘ ┴ └───┘
src ┴ └─┘ ┴ └──┘ ┴ └──┘ └──────────┘ └───┘
typ └┘ ┴ └┘ └─┘ ┴ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴ └──────────┘ ┴ └───┘
doc └──┘ └─┘ └──┘ └──┘
330 @[simp] lemma map_infi {m : ι → measurable_space α} : (⨅i, m i).map f = (⨅i, (m i).map f) :=
id ┴ └──────────────┘ ┴ ┴┴┴ ┴ ┴ └─┘ ┴ ┴ ┴┴┴ ┴ ┴ └─┘ ┴
src └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
typ ┴ └──────────────┘ ┴ ┴┴┴ ┴ ┴ └─┘ ┴ ┴ ┴┴┴ ┴ ┴ └─┘ ┴
doc └──┘ ┴ ┴ └─┘ ┴ ┴ └─┘
331 (gc_comap_map f).u_infi
id └──────────┘ ┴ └────┘
src └──────────┘ └────┘
typ └──────────┘ ┴ └────┘
332
333 lemma comap_map_le : (m.map f).comap f ≤ m := (gc_comap_map f).l_u_le _
id ┴└──┘ ┴ └───┘ ┴ ┴ ┴ └──────────┘ ┴ └────┘
src └──┘ └───┘ ┴ └──────────┘ └────┘
typ ┴└──┘ ┴ └───┘ ┴ ┴ ┴ └──────────┘ ┴ └────┘
doc └──┘ └───┘
334 lemma le_map_comap : m ≤ (m.comap g).map g := (gc_comap_map g).le_u_l _
id ┴ ┴ ┴└────┘ ┴ └─┘ ┴ └──────────┘ ┴ └────┘
src ┴ └────┘ └─┘ └──────────┘ └────┘
typ ┴ ┴ ┴└────┘ ┴ └─┘ ┴ └──────────┘ ┴ └────┘
doc └────┘ └─┘
335
336 end functors
337
338 lemma generate_from_le_generate_from {s t : set (set α)} (h : s ⊆ t) :
id └─┘ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴
typ └─┘ └─┘ ┴ ┴ ┴ ┴
339 generate_from s ≤ generate_from t :=
id └───────────┘ ┴ ┴ └───────────┘ ┴
src └───────────┘ ┴ └───────────┘
typ └───────────┘ ┴ ┴ └───────────┘ ┴
doc └───────────┘ └───────────┘
340 gi_generate_from.gc.monotone_l h
id └──────────────┘└─┘└─────────┘ ┴
src └──────────────┘└─┘└─────────┘
typ └──────────────┘└─┘└─────────┘ ┴
341
342 lemma generate_from_sup_generate_from {s t : set (set α)} :
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
343 generate_from s ⊔ generate_from t = generate_from (s ∪ t) :=
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────┘ └───────────┘
344 (@gi_generate_from α).gc.l_sup.symm
id └──────────────┘ ┴ └┘ └───┘ └──┘
src └──────────────┘ └┘ └───┘ └──┘
typ └──────────────┘ ┴ └┘ └───┘ └──┘
345
346 lemma comap_generate_from {f : α → β} {s : set (set β)} :
id ┴ ┴ └─┘ └─┘ ┴
src └─┘ └─┘
typ ┴ ┴ └─┘ └─┘ ┴
347 (generate_from s).comap f = generate_from (preimage f '' s) :=
id └───────────┘ ┴ └───┘ ┴ ┴ └───────────┘ └──────┘ ┴ └┘ ┴
src └───────────┘ └───┘ ┴ └───────────┘ └──────┘ └┘
typ └───────────┘ ┴ └───┘ ┴ ┴ └───────────┘ └──────┘ ┴ └┘ ┴
doc └───────────┘ └───┘ └───────────┘ └──────┘
348 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
349 (comap_le_iff_le_map.2 $ generate_from_le $ assume t hts,
id └─────────────────┘┴ └──────────────┘ ┴ └─┘
src └─────────────────┘┴ └──────────────┘
typ └─────────────────┘┴ └──────────────┘ ┴ └─┘
350 generate_measurable.basic _ $ mem_image_of_mem _ $ hts)
id └───────────────────────┘ └──────────────┘ └─┘
src └───────────────────────┘ └──────────────┘
typ └───────────────────────┘ └──────────────┘ └─┘
351 (generate_from_le $ assume t ⟨u, hu, eq⟩, eq ▸ ⟨u, generate_measurable.basic _ hu, rfl⟩)
id └──────────────┘ ┴ ┴┴ └┘ └┘ ┴ └───────────────────────┘ └─┘
src └──────────────┘ └┘ ┴ └───────────────────────┘ └─┘
typ └──────────────┘ ┴ ┴┴ └┘ └┘ ┴ └───────────────────────┘ └─┘
352
353 end measurable_space
354
355 section measurable_functions
356 open measurable_space
357
358 /-- A function `f` between measurable spaces is measurable if the preimage of every
359 measurable set is measurable. -/
360 def measurable [m₁ : measurable_space α] [m₂ : measurable_space β] (f : α → β) : Prop :=
id └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
361 m₂ ≤ m₁.map f
id └┘ ┴ └┘└──┘ ┴
src ┴ └──┘
typ └┘ ┴ └┘└──┘ ┴
doc └──┘
362
363 lemma measurable_id [measurable_space α] : measurable (@id α) := le_refl _
id └──────────────┘ ┴ └────────┘ └┘ ┴ └─────┘
src └──────────────┘ └────────┘ └┘ └─────┘
typ └──────────────┘ ┴ └────────┘ └┘ ┴ └─────┘
doc └────────┘
364
365 lemma measurable.preimage [measurable_space α] [measurable_space β]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
366 {f : α → β} (hf : measurable f) {s : set β} : is_measurable s → is_measurable (f ⁻¹' s) := hf _
id ┴ ┴ └────────┘ ┴ └─┘ ┴ └───────────┘ ┴ └───────────┘ ┴ └─┘ ┴ └┘
src └────────┘ └─┘ └───────────┘ └───────────┘ └─┘
typ ┴ ┴ └────────┘ ┴ └─┘ ┴ └───────────┘ ┴ └───────────┘ ┴ └─┘ ┴ └┘
doc └────────┘ └───────────┘ └───────────┘ └─┘
367
368 lemma measurable.comp [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
369 {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) : measurable (g ∘ f) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
370 le_trans hg $ map_mono hf
id └──────┘ └┘ └──────┘ └┘
src └──────┘ └──────┘
typ └──────┘ └┘ └──────┘ └┘
371
372 lemma measurable_generate_from [measurable_space α] {s : set (set β)} {f : α → β}
id └──────────────┘ ┴ └─┘ └─┘ ┴ ┴ ┴
src └──────────────┘ └─┘ └─┘
typ └──────────────┘ ┴ └─┘ └─┘ ┴ ┴ ┴
373 (h : ∀t∈s, is_measurable (f ⁻¹' t)) : @measurable _ _ _ (generate_from s) f :=
id ┴ ┴ └───────────┘ ┴ └─┘ ┴ └────────┘ └───────────┘ ┴ ┴
src └───────────┘ └─┘ └────────┘ └───────────┘
typ ┴ ┴ └───────────┘ ┴ └─┘ ┴ └────────┘ └───────────┘ ┴ ┴
doc └───────────┘ └─┘ └────────┘ └───────────┘
374 generate_from_le h
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
375
376 lemma measurable.if [measurable_space α] [measurable_space β]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
377 {p : α → Prop} {h : decidable_pred p} {f g : α → β}
id ┴ └────────────┘ ┴ ┴ ┴
src └────────────┘
typ ┴ └────────────┘ ┴ ┴ ┴
378 (hp : is_measurable {a | p a}) (hf : measurable f) (hg : measurable g) :
id └───────────┘ ┴┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └───────────┘ ┴ └────────┘ └────────┘
typ └───────────┘ ┴┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └───────────┘ └────────┘ └────────┘
379 measurable (λa, if p a then f a else g a) :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
380 λ s hs, show is_measurable {a | (if p a then f a else g a) ∈ s},
id ┴ └┘ └───────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ ┴ └┘ └───────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
381 begin
st └─────
382 convert (hp.inter $ hf s hs).union (hp.compl.inter $ hg s hs),
id └──────┘ └┘ └────────────┘ └┘ ┴ └┘
src └──────┘ └──────┘┴ ┴ ┴ ┴ └──────┘ └────────────┘┴ ┴ ┴ ┴ ┴
typ └──────┘ └──────┘┴ ┴└┘┴ ┴ └──────┘ └────────────┘┴ ┴└┘┴┴┴└┘┴
doc └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
383 exact ext (λ a, by by_cases p a ; { rw mem_def, simp [h] })
id └─┘ ┴ ┴ └─────┘ ┴
src └────┘└─┘┴ └──┘ ┴└───────┘ ┴ ┴└──┘└─┘└─────┘└┘└────┘ └┘└─┘
typ └────┘└─┘┴ └──┘ ┴└───────┘┴┴┴┴└──┘└─┘└─────┘└┘└────┘┴└┘└─┘
doc └────┘ ┴ └──┘ ┴└───────┘ ┴ ┴└──┘└─┘ └┘└────┘ └┘└─┘
txt └────┘ ┴ └──┘ ┴└───────┘ ┴ ┴└──┘└─┘ └┘└────┘ └┘└─┘
par └────┘ ┴ └──┘ ┴└───────┘ ┴ ┴└──┘└─┘ └┘└────┘ └┘└─┘
pid ┴ ┴ └──┘ └────────┘ ┴ └──────┘ └──────┘ └──┘┴
st ───────────────────┘└───────────────┘└─────────┘└─────────┘┴└┘
384 end
st └─┘
385
386 lemma measurable_const {α β} [measurable_space α] [measurable_space β] {a : α} : measurable (λb:β, a) :=
id └──────────────┘ ┴ └──────────────┘ ┴ ┴ └────────┘ ┴ ┴
src └──────────────┘ └──────────────┘ └────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘
387 assume s hs, show is_measurable {b : β | a ∈ s}, from
id ┴ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ ┴ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
388 classical.by_cases
id └────────────────┘
src └────────────────┘
typ └────────────────┘
389 (assume h : a ∈ s, by simp [h]; from is_measurable.univ)
id ┴ ┴ ┴ ┴ └────────────────┘
src ┴ └────┘ ┴ └───┘└────────────────┘
typ ┴ ┴ ┴ └────┘┴┴ └───┘└────────────────┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴┴ ┴ └───┘
st └────────────────────────────────┘
390 (assume h : a ∉ s, by simp [h]; from is_measurable.empty)
id ┴ ┴ ┴ ┴ └─────────────────┘
src ┴ └────┘ ┴ └───┘└─────────────────┘
typ ┴ ┴ ┴ └────┘┴┴ └───┘└─────────────────┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴┴ ┴ └───┘
st └─────────────────────────────────┘
391
392 lemma measurable_zero {α β} [measurable_space α] [has_zero α] [measurable_space β] :
id └──────────────┘ ┴ └──────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────┘ └──────────────┘
typ └──────────────┘ ┴ └──────┘ ┴ └──────────────┘ ┴
393 measurable (λb:β, (0:α)) := measurable_const
id └────────┘ ┴ ┴ └──────────────┘
src └────────┘ └──────────────┘
typ └────────┘ ┴ ┴ └──────────────┘
doc └────────┘
394
395 end measurable_functions
396
397 section constructions
398
399 instance : measurable_space empty := ⊤
id └──────────────┘ └───┘ ┴
src └──────────────┘ └───┘ ┴
typ └──────────────┘ └───┘ ┴
400 instance : measurable_space unit := ⊤
id └──────────────┘ └──┘ ┴
src └──────────────┘ └──┘ ┴
typ └──────────────┘ └──┘ ┴
doc └──┘
401 instance : measurable_space bool := ⊤
id └──────────────┘ └──┘ ┴
src └──────────────┘ └──┘ ┴
typ └──────────────┘ └──┘ ┴
402 instance : measurable_space ℕ := ⊤
id └──────────────┘ ┴ ┴
src └──────────────┘ ┴ ┴
typ └──────────────┘ ┴ ┴
403 instance : measurable_space ℤ := ⊤
id └──────────────┘ ┴ ┴
src └──────────────┘ ┴ ┴
typ └──────────────┘ ┴ ┴
404
405 lemma measurable_unit [measurable_space α] (f : unit → α) : measurable f :=
id └──────────────┘ ┴ └──┘ ┴ └────────┘ ┴
src └──────────────┘ └──┘ └────────┘
typ └──────────────┘ ┴ └──┘ ┴ └────────┘ ┴
doc └──┘ └────────┘
406 have f = (λu, f ()) := funext $ assume ⟨⟩, rfl,
id ┴ ┴ ┴ ┴ └┘ └────┘ ┴ └─┘
src ┴ └┘ └────┘ ┴ └─┘
typ ┴ ┴ ┴ ┴ └┘ └────┘ ┴ └─┘
407 by rw this; exact measurable_const
id └──┘ └──────────────┘
src └─┘ └────┘└──────────────┘└
typ └─┘└──┘ └────┘└──────────────┘└
doc └─┘ └────┘ └
txt └─┘ └────┘ └
par └─┘ └────┘ └
pid ┴ ┴ └
st └────────────────────────────────
408
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
409 section nat
410
411 lemma measurable_from_nat [measurable_space α] {f : ℕ → α} : measurable f :=
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴
src └──────────────┘ ┴ └────────┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘
412 assume s hs, show is_measurable {n : ℕ | f n ∈ s}, from trivial
id ┴ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └───────────┘ ┴ ┴ ┴ └─────┘
typ ┴ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └───────────┘
413
414 lemma measurable_to_nat [measurable_space α] {f : α → ℕ} :
id └──────────────┘ ┴ ┴ ┴
src └──────────────┘ ┴
typ └──────────────┘ ┴ ┴ ┴
415 (∀ k, is_measurable {x | f x = k}) → measurable f :=
id ┴ └───────────┘ ┴┴ ┴ ┴ ┴ ┴ └────────┘ ┴
src └───────────┘ ┴ ┴ └────────┘
typ ┴ └───────────┘ ┴┴ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └───────────┘ └────────┘
416 begin
st └─────
417 assume h s hs, show is_measurable {x | f x ∈ s},
id └───────────┘ ┴ ┴ ┴ ┴
src └───────────┘ └───┘└───────────┘┴┴└──┘ ┴ ┴┴┴ ┴
typ └───────────┘ └───┘└───────────┘┴┴└──┘┴┴ ┴┴┴┴┴
doc └───────────┘ └───┘└───────────┘┴ └──┘ ┴ ┴ ┴ ┴
txt └───────────┘ └───┘ ┴ └──┘ ┴ ┴ ┴ ┴
par └───────────┘ └───┘ ┴ └──┘ ┴ ┴ ┴ ┴
pid └───────────┘ └───┘ ┴ └──┘ ┴ ┴ ┴ ┴
st ──────────────┘└────────────────────────────────┘└─
418 have : {x | f x ∈ s} = ⋃ (n ∈ s), {x | f x = n}, { ext, simp },
id ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ ┴ ┴ ┴ └┘┴┴┴└────┘ ┴┴┴┴└──┘ ┴ ┴ ┴ ┴ └─┘ └───┘
typ └─────┘ └──┘ ┴ ┴ ┴ └┘┴┴┴└────┘┴┴┴┴┴└──┘┴┴ ┴ ┴ ┴ └─┘ └───┘
doc └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴┴└────┘ ┴┴┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └───┘
txt └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └───┘
par └─────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ └───┘
pid └───┘└┘ └──┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────┘└──┘└─┘└─────┘└┘└
419 rw this, simp [is_measurable.Union, is_measurable.Union_Prop, h]
id └──┘ └─────────────────┘ └──────────────────────┘ ┴
src └─┘ └────┘└─────────────────┘└┘└──────────────────────┘└┘ └┘
typ └─┘└──┘ └────┘└─────────────────┘└┘└──────────────────────┘└┘┴└┘
doc └─┘ └────┘ └┘ └┘ └┘
txt └─┘ └────┘ └┘ └┘ └┘
par └─┘ └────┘ └┘ └┘ └┘
pid ┴ ┴┴ └┘ └┘ ┴┴
st ────────┘└────────────────────────────────────────────────────────┘
420 end
st └─┘
421
422 lemma measurable_find_greatest [measurable_space α] {p : ℕ → α → Prop} :
id └──────────────┘ ┴ ┴ ┴
src └──────────────┘ ┴
typ └──────────────┘ ┴ ┴ ┴
423 ∀ {N}, (∀ k ≤ N, is_measurable {x | nat.find_greatest (λ n, p n x) N = k}) →
id ┴┴ ┴ ┴ └───────────┘ ┴┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────────┘ ┴ └───────────────┘ ┴
typ ┴┴ ┴ ┴ └───────────┘ ┴┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘ └───────────────┘
424 measurable (λ x, nat.find_greatest (λ n, p n x) N)
id └────────┘ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ └───────────────┘
typ └────────┘ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └───────────────┘
425 | 0 := assume h s hs, show is_measurable {x : α | (nat.find_greatest (λ n, p n x) 0) ∈ s},
id ┴ ┴ └┘ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ └───────────────┘ ┴
typ ┴ ┴ └┘ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘ └───────────────┘
426 begin
st └─────
427 by_cases h : 0 ∈ s,
id ┴ ┴
src └───────┘ └───┘┴┴
typ └───────┘ └───┘┴┴┴
doc └───────┘ └───┘ ┴
txt └───────┘ └───┘ ┴
par └───────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ───────────────────┘└─
428 { convert is_measurable.univ, simp only [nat.find_greatest_zero, h] },
id └────────────────┘ └────────────────────┘ ┴
src └──────┘└────────────────┘ └─────────┘└────────────────────┘└┘ └┘
typ └──────┘└────────────────┘ └─────────┘└────────────────────┘└┘┴└┘
doc └──────┘ └─────────┘ └┘ └┘
txt └──────┘ └─────────┘ └┘ └┘
par └──────┘ └─────────┘ └┘ └┘
pid ┴ ┴└──┘└┘ └┘ ┴┴
st ───┘└────────────────────────┘└──────────────────────────────────────┘└┘└
429 { convert is_measurable.empty, simp only [nat.find_greatest_zero, h], refl }
id └─────────────────┘ └────────────────────┘ ┴
src └──────┘└─────────────────┘ └─────────┘└────────────────────┘└┘ ┴ └───┘
typ └──────┘└─────────────────┘ └─────────┘└────────────────────┘└┘┴┴ └───┘
doc └──────┘ └─────────┘ └┘ ┴ └───┘
txt └──────┘ └─────────┘ └┘ ┴ └───┘
par └──────┘ └─────────┘ └┘ ┴ └───┘
pid ┴ ┴└──┘└┘ └┘ ┴ ┴
st ──────────────────────────────┘└─────────────────────────────────────┘└─────┘└─
430 end
st ──┘
431 | (n + 1) := assume h,
id ┴ ┴
src ┴
typ ┴ ┴
432 begin
st └─────
433 apply measurable_to_nat, assume k, by_cases hk : k ≤ n + 1,
id └───────────────┘ ┴ ┴ ┴ ┴
src └────┘└───────────────┘ └──────┘ └───────┘ └─┘ ┴┴┴ ┴┴└┘
typ └────┘└───────────────┘ └──────┘ └───────┘ └─┘┴┴┴┴┴┴┴└┘
doc └────┘ └──────┘ └───────┘ └─┘ ┴ ┴ ┴ └┘
txt └────┘ └──────┘ └───────┘ └─┘ ┴ ┴ ┴ └┘
par └────┘ └──────┘ └───────┘ └─┘ ┴ ┴ ┴ └┘
pid ┴ └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴┴
st ────────────────────────┘└────────┘└───────────────────────┘└─
434 { exact h k hk },
id ┴ ┴ └┘
src └────┘ ┴ ┴ ┴
typ └────┘┴┴┴┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───┘└───────────┘└┘└
435 { have := is_measurable.empty, rw ← set_of_false at this, convert this, funext, rw eq_false,
id └─────────────────┘ └──────────┘ └──┘ └──────┘
src └──────┘└─────────────────┘ └───┘└──────────┘└──────┘ └──────┘ └────┘ └─┘└──────┘
typ └──────┘└─────────────────┘ └───┘└──────────┘└──────┘ └──────┘└──┘ └────┘ └─┘└──────┘
doc └──────┘ └───┘ └──────┘ └──────┘ └────┘ └─┘
txt └──────┘ └───┘ └──────┘ └──────┘ └────┘ └─┘
par └──────┘ └───┘ └──────┘ └──────┘ └────┘ └─┘
pid └───┘└─┘ └─┘ └──────┘ ┴ ┴
st ──────────────────────────────┘└─────────────────────────┘└────────────┘└──────┘└───────────┘└─
436 assume h, rw ← h at hk, have := nat.find_greatest_le, contradiction }
id ┴ └──────────────────┘
src └──────┘ └───┘ └────┘ └──────┘└──────────────────┘ └────────────┘
typ └──────┘ └───┘┴└────┘ └──────┘└──────────────────┘ └────────────┘
doc └──────┘ └───┘ └────┘ └──────┘ └────────────┘
txt └──────┘ └───┘ └────┘ └──────┘ └────────────┘
par └──────┘ └───┘ └────┘ └──────┘ └────────────┘
pid └──────┘ └─┘ └────┘ └───┘└─┘ ┴
st ───────────┘└────────────┘└────────────────────────────┘└──────────────┘└─
437 end
st ──┘
438
439 end nat
440
441 section subtype
442
443 instance {p : α → Prop} [m : measurable_space α] : measurable_space (subtype p) :=
id ┴ └──────────────┘ ┴ └──────────────┘ └─────┘ ┴
src └──────────────┘ └──────────────┘ └─────┘
typ ┴ └──────────────┘ ┴ └──────────────┘ └─────┘ ┴
444 m.comap subtype.val
id ┴└────┘ └─────────┘
src └────┘ └─────────┘
typ ┴└────┘ └─────────┘
doc └────┘
445
446 lemma measurable.subtype_val [measurable_space α] [measurable_space β] {p : β → Prop}
id └──────────────┘ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ ┴
447 {f : α → subtype p} (hf : measurable f) : measurable (λa:α, (f a).val) :=
id ┴ └─────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ └─┘
src └─────┘ └────────┘ └────────┘ └─┘
typ ┴ └─────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ └─┘
doc └────────┘ └────────┘
448 measurable.comp (measurable_space.comap_le_iff_le_map.mp (le_refl _)) hf
id └─────────────┘ └──────────────────────────────────┘└─┘ └─────┘ └┘
src └─────────────┘ └──────────────────────────────────┘└─┘ └─────┘
typ └─────────────┘ └──────────────────────────────────┘└─┘ └─────┘ └┘
449
450 lemma measurable.subtype_mk [measurable_space α] [measurable_space β] {p : β → Prop}
id └──────────────┘ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ ┴
451 {f : α → subtype p} (hf : measurable (λa, (f a).val)) : measurable f :=
id ┴ └─────┘ ┴ └────────┘ ┴ ┴ ┴ └─┘ └────────┘ ┴
src └─────┘ └────────┘ └─┘ └────────┘
typ ┴ └─────┘ ┴ └────────┘ ┴ ┴ ┴ └─┘ └────────┘ ┴
doc └────────┘ └────────┘
452 measurable_space.comap_le_iff_le_map.mpr $ by rw [measurable_space.map_comp]; exact hf
id └──────────────────────────────────┘└──┘ └───────────────────────┘ └┘
src └──────────────────────────────────┘└──┘ └──┘└───────────────────────┘┴ └────┘ └
typ └──────────────────────────────────┘└──┘ └──┘└───────────────────────┘┴ └────┘└┘└
doc └──┘ ┴ └────┘ └
txt └──┘ ┴ └────┘ └
par └──┘ ┴ └────┘ └
pid └┘ ┴ ┴ └
st └────────────────────────────┘┴└──────────
453
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
454 lemma is_measurable_subtype_image [measurable_space α] {s : set α} {t : set s}
id └──────────────┘ ┴ └─┘ ┴ └─┘ ┴
src └──────────────┘ └─┘ └─┘
typ └──────────────┘ ┴ └─┘ ┴ └─┘ ┴
455 (hs : is_measurable s) : is_measurable t → is_measurable ((coe : s → α) '' t)
id └───────────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ └─┘ ┴ ┴ └┘ ┴
src └───────────┘ └───────────┘ └───────────┘ └─┘ └┘
typ └───────────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ └─┘ ┴ ┴ └┘ ┴
doc └───────────┘ └───────────┘ └───────────┘
456 | ⟨u, (hu : is_measurable u), (eq : coe ⁻¹' u = t)⟩ :=
id └───────────┘ └─┘ └─┘ ┴ ┴
src └───────────┘ └─┘ └─┘ ┴
typ └───────────┘ └─┘ └─┘ ┴ ┴
doc └───────────┘ └─┘
457 begin
st └─────
458 rw [← eq, image_preimage_eq_inter_range, range_coe_subtype],
id └┘ └───────────────────────────┘ └───────────────┘
src └────┘└┘└┘└───────────────────────────┘└┘└───────────────┘┴
typ └────┘└┘└┘└───────────────────────────┘└┘└───────────────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid └──┘ └┘ └┘ ┴
st ───────────┘└─────────────────────────────┘└─────────────────┘└──
459 exact is_measurable.inter hu hs
id └─────────────────┘ └┘ └┘
src └────┘└─────────────────┘┴ ┴ └
typ └────┘└─────────────────┘┴└┘┴└┘└
doc └────┘ ┴ ┴ └
txt └────┘ ┴ ┴ └
par └────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ────────────────────────────────────
460 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
461
462 lemma measurable_of_measurable_union_cover
463 [measurable_space α] [measurable_space β]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
464 {f : α → β} (s t : set α) (hs : is_measurable s) (ht : is_measurable t) (h : univ ⊆ s ∪ t)
id ┴ ┴ └─┘ ┴ └───────────┘ ┴ └───────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
src └─┘ └───────────┘ └───────────┘ └──┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ └───────────┘ ┴ └───────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
doc └───────────┘ └───────────┘
465 (hc : measurable (λa:s, f a)) (hd : measurable (λa:t, f a)) :
id └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src └────────┘ └────────┘
typ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └────────┘ └────────┘
466 measurable f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
467 assume u (hu : is_measurable u), show is_measurable (f ⁻¹' u), from
id ┴ └───────────┘ ┴ └───────────┘ ┴ └─┘ ┴
src └───────────┘ └───────────┘ └─┘
typ ┴ └───────────┘ ┴ └───────────┘ ┴ └─┘ ┴
doc └───────────┘ └───────────┘ └─┘
468 begin
st └─────
469 rw show f ⁻¹' u = coe '' (coe ⁻¹' (f ⁻¹' u) : set s) ∪ coe '' (coe ⁻¹' (f ⁻¹' u) : set t),
id └─┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴└─┘┴ ┴┴┴ ┴└┘┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘┴┴ ┴ ┴ └─┘┴ ┴ ┴ ┴ └──┘└─┘┴ └──
typ └─┘ ┴ ┴└─┘┴ ┴┴┴ ┴└┘┴ ┴ ┴ ┴ ┴ └──┘ ┴┴└┘┴┴ ┴ ┴ └─┘┴ ┴ ┴┴ ┴┴└──┘└─┘┴┴└──
doc └─┘ ┴ ┴└─┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
txt └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
par └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──
st ─────────────────────────────────────────────────────────────────────────────────────────────
470 by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, range_coe_subtype, range_coe_subtype, ← inter_distrib_left, univ_subset_iff.1 h, inter_univ],
id └───────────────────────────┘ └───────────────────────────┘ └───────────────┘ └───────────────┘ └────────────────┘ └─────────────┘ ┴ └────────┘
src ──────────┘└───────────────────────────┘└┘└───────────────────────────┘└┘└───────────────┘└┘└───────────────┘└──┘└────────────────┘└┘└─────────────┘└─┘ └┘└────────┘┴
typ ──────────┘└───────────────────────────┘└┘└───────────────────────────┘└┘└───────────────┘└┘└───────────────┘└──┘└────────────────┘└┘└─────────────┘└─┘┴└┘└────────┘┴
doc ──────────┘ └┘ └┘ └┘ └──┘ └┘ └─┘ └┘ ┴
txt ──────────┘ └┘ └┘ └┘ └──┘ └┘ └─┘ └┘ ┴
par ──────────┘ └┘ └┘ └┘ └──┘ └┘ └─┘ └┘ ┴
pid ──────────┘ └┘ └┘ └┘ └──┘ └┘ └─┘ └┘ ┴
st ─────┘└────────────────────────────────┘└─────────────────────────────┘└─────────────────┘└─────────────────┘└────────────────────┘└───────────────────┘└──────────┘┴└─
471 exact is_measurable.union
id └─────────────────┘
src └────┘└─────────────────┘└
typ └────┘└─────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ────────────────────────────
472 (is_measurable_subtype_image hs (hc _ hu))
id └┘ └┘
src ───┘ ┴ ┴ └─┘ └──
typ ───┘ ┴└┘┴ └┘└─┘ └──
doc ───┘ ┴ ┴ └─┘ └──
txt ───┘ ┴ ┴ └─┘ └──
par ───┘ ┴ ┴ └─┘ └──
pid ───┘ ┴ ┴ └─┘ └──
st ───────────────────────────────────────────────
473 (is_measurable_subtype_image ht (hd _ hu))
id └─────────────────────────┘ └┘ └┘ └┘
src ───┘ └─────────────────────────┘┴ ┴ └─┘ └─┘
typ ───┘ └─────────────────────────┘┴└┘┴ └┘└─┘└┘└─┘
doc ───┘ ┴ ┴ └─┘ └─┘
txt ───┘ ┴ ┴ └─┘ └─┘
par ───┘ ┴ ┴ └─┘ └─┘
pid ───┘ ┴ ┴ └─┘ └┘┴
st ──────────────────────────────────────────────┘
474 end
st └─┘
475
476 end subtype
477
478 section prod
479
480 instance [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α × β) :=
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
src └──────────────┘ └──────────────┘ └──────────────┘ ┴
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
481 m₁.comap prod.fst ⊔ m₂.comap prod.snd
id └┘└────┘ └──────┘ ┴ └┘└────┘ └──────┘
src └────┘ └──────┘ ┴ └────┘ └──────┘
typ └┘└────┘ └──────┘ ┴ └┘└────┘ └──────┘
doc └────┘ └────┘
482
483 lemma measurable.fst [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
484 {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).1) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src ┴ └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
485 measurable.comp (measurable_space.comap_le_iff_le_map.mp le_sup_left) hf
id └─────────────┘ └──────────────────────────────────┘└─┘ └─────────┘ └┘
src └─────────────┘ └──────────────────────────────────┘└─┘ └─────────┘
typ └─────────────┘ └──────────────────────────────────┘└─┘ └─────────┘ └┘
486
487 lemma measurable.snd [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
488 {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).2) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src ┴ └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
489 measurable.comp (measurable_space.comap_le_iff_le_map.mp le_sup_right) hf
id └─────────────┘ └──────────────────────────────────┘└─┘ └──────────┘ └┘
src └─────────────┘ └──────────────────────────────────┘└─┘ └──────────┘
typ └─────────────┘ └──────────────────────────────────┘└─┘ └──────────┘ └┘
490
491 lemma measurable.prod [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
492 {f : α → β × γ} (hf₁ : measurable (λa, (f a).1)) (hf₂ : measurable (λa, (f a).2)) :
id ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src ┴ └────────┘ ┴ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘
493 measurable f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
494 sup_le
id └────┘
src └────┘
typ └────┘
495 (by rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp]; exact hf₁)
id └──────────────────────────────────┘ └───────────────────────┘ └─┘
src └──┘└──────────────────────────────────┘└┘└───────────────────────┘┴ └────┘
typ └──┘└──────────────────────────────────┘└┘└───────────────────────┘┴ └────┘└─┘
doc └──┘ └┘ ┴ └────┘
txt └──┘ └┘ ┴ └────┘
par └──┘ └┘ ┴ └────┘
pid └┘ └┘ ┴ ┴
st └───────────────────────────────────────┘└─────────────────────────┘┴└─────────┘
496 (by rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp]; exact hf₂)
id └──────────────────────────────────┘ └───────────────────────┘ └─┘
src └──┘└──────────────────────────────────┘└┘└───────────────────────┘┴ └────┘
typ └──┘└──────────────────────────────────┘└┘└───────────────────────┘┴ └────┘└─┘
doc └──┘ └┘ ┴ └────┘
txt └──┘ └┘ ┴ └────┘
par └──┘ └┘ ┴ └────┘
pid └┘ └┘ ┴ ┴
st └───────────────────────────────────────┘└─────────────────────────┘┴└─────────┘
497
498 lemma measurable.prod_mk [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
499 {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) : measurable (λa:α, (f a, g a)) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
500 measurable.prod hf hg
id └─────────────┘ └┘ └┘
src └─────────────┘
typ └─────────────┘ └┘ └┘
501
502 lemma is_measurable_set_prod [measurable_space α] [measurable_space β] {s : set α} {t : set β}
id └──────────────┘ ┴ └──────────────┘ ┴ └─┘ ┴ └─┘ ┴
src └──────────────┘ └──────────────┘ └─┘ └─┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └─┘ ┴ └─┘ ┴
503 (hs : is_measurable s) (ht : is_measurable t) : is_measurable (set.prod s t) :=
id └───────────┘ ┴ └───────────┘ ┴ └───────────┘ └──────┘ ┴ ┴
src └───────────┘ └───────────┘ └───────────┘ └──────┘
typ └───────────┘ ┴ └───────────┘ ┴ └───────────┘ └──────┘ ┴ ┴
doc └───────────┘ └───────────┘ └───────────┘ └──────┘
504 is_measurable.inter (measurable.fst measurable_id _ hs) (measurable.snd measurable_id _ ht)
id └─────────────────┘ └────────────┘ └───────────┘ └┘ └────────────┘ └───────────┘ └┘
src └─────────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
typ └─────────────────┘ └────────────┘ └───────────┘ └┘ └────────────┘ └───────────┘ └┘
505
506 end prod
507
508 section pi
509
510 instance measurable_space.pi {α : Type u} {β : α → Type v} [m : Πa, measurable_space (β a)] :
id ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘
typ ┴ ┴ └──────────────┘ ┴ ┴
511 measurable_space (Πa, β a) :=
id └──────────────┘ ┴ ┴ ┴
src └──────────────┘
typ └──────────────┘ ┴ ┴ ┴
512 ⨆a, (m a).comap (λb, b a)
id ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴
src ┴ ┴ └───┘
typ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc ┴ ┴ └───┘
513
514 lemma measurable_pi_apply {α : Type u} {β : α → Type v} [Πa, measurable_space (β a)] (a : α) :
id ┴ ┴ └──────────────┘ ┴ ┴ ┴
src └──────────────┘
typ ┴ ┴ └──────────────┘ ┴ ┴ ┴
515 measurable (λf:Πa, β a, f a) :=
id └────────┘ ┴ ┴ ┴ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘
516 measurable_space.comap_le_iff_le_map.1 $ lattice.le_supr _ a
id └──────────────────────────────────┘┴ └─────────────┘ ┴
src └──────────────────────────────────┘┴ └─────────────┘
typ └──────────────────────────────────┘┴ └─────────────┘ ┴
517
518 lemma measurable_pi_lambda {α : Type u} {β : α → Type v} {γ : Type w}
id ┴
typ ┴
519 [Πa, measurable_space (β a)] [measurable_space γ]
id ┴ └──────────────┘ ┴ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ ┴ └──────────────┘ ┴ ┴ └──────────────┘ ┴
520 (f : γ → Πa, β a) (hf : ∀a, measurable (λc, f c a)) :
id ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src └────────┘
typ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────────┘
521 measurable f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
522 lattice.supr_le $ assume a, measurable_space.comap_le_iff_le_map.2 (hf a)
id └─────────────┘ ┴ └──────────────────────────────────┘┴ └┘ ┴
src └─────────────┘ └──────────────────────────────────┘┴
typ └─────────────┘ ┴ └──────────────────────────────────┘┴ └┘ ┴
523
524 end pi
525
526 instance [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α ⊕ β) :=
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
src └──────────────┘ └──────────────┘ └──────────────┘ ┴
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
527 m₁.map sum.inl ⊓ m₂.map sum.inr
id └┘└──┘ └─────┘ ┴ └┘└──┘ └─────┘
src └──┘ └─────┘ ┴ └──┘ └─────┘
typ └┘└──┘ └─────┘ ┴ └┘└──┘ └─────┘
doc └──┘ └──┘
528
529 section sum
530 variables [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ └──────────────┘ └──────────────┘
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ └──────────────┘ └──────────────┘
531
532 lemma measurable_inl : measurable (@sum.inl α β) := inf_le_left
id └────────┘ └─────┘ ┴ ┴ └─────────┘
src └────────┘ └─────┘ └─────────┘
typ └────────┘ └─────┘ ┴ ┴ └─────────┘
doc └────────┘
533
534 lemma measurable_inr : measurable (@sum.inr α β) := inf_le_right
id └────────┘ └─────┘ ┴ ┴ └──────────┘
src └────────┘ └─────┘ └──────────┘
typ └────────┘ └─────┘ ┴ ┴ └──────────┘
doc └────────┘
535
536 lemma measurable_sum {f : α ⊕ β → γ}
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
537 (hl : measurable (f ∘ sum.inl)) (hr : measurable (f ∘ sum.inr)) : measurable f :=
id └────────┘ ┴ ┴ └─────┘ └────────┘ ┴ ┴ └─────┘ └────────┘ ┴
src └────────┘ ┴ └─────┘ └────────┘ ┴ └─────┘ └────────┘
typ └────────┘ ┴ ┴ └─────┘ └────────┘ ┴ ┴ └─────┘ └────────┘ ┴
doc └────────┘ └────────┘ └────────┘
538 measurable_space.comap_le_iff_le_map.1 $ le_inf
id └──────────────────────────────────┘┴ └────┘
src └──────────────────────────────────┘┴ └────┘
typ └──────────────────────────────────┘┴ └────┘
539 (measurable_space.comap_le_iff_le_map.2 $ hl)
id └──────────────────────────────────┘┴ └┘
src └──────────────────────────────────┘┴
typ └──────────────────────────────────┘┴ └┘
540 (measurable_space.comap_le_iff_le_map.2 $ hr)
id └──────────────────────────────────┘┴ └┘
src └──────────────────────────────────┘┴
typ └──────────────────────────────────┘┴ └┘
541
542 lemma measurable_sum_rec {f : α → γ} {g : β → γ}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
543 (hf : measurable f) (hg : measurable g) : @measurable (α ⊕ β) γ _ _ (@sum.rec α β (λ_, γ) f g) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴ └─────┘
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────┘ └────────┘
544 measurable_sum hf hg
id └────────────┘ └┘ └┘
src └────────────┘
typ └────────────┘ └┘ └┘
545
546 lemma is_measurable_inl_image {s : set α} (hs : is_measurable s) :
id └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
547 is_measurable (sum.inl '' s : set (α ⊕ β)) :=
id └───────────┘ └─────┘ └┘ ┴ └─┘ ┴ ┴ ┴
src └───────────┘ └─────┘ └┘ └─┘ ┴
typ └───────────┘ └─────┘ └┘ ┴ └─┘ ┴ ┴ ┴
doc └───────────┘
548 ⟨show is_measurable (sum.inl ⁻¹' _), by rwa [preimage_image_eq]; exact (assume a b, sum.inl.inj),
id └───────────┘ └─────┘ └─┘ └───────────────┘ └─────────┘
src └───────────┘ └─────┘ └─┘ └───┘└───────────────┘┴ └────┘ └────┘└─────────┘┴
typ └───────────┘ └─────┘ └─┘ └───┘└───────────────┘┴ └────┘ └────┘└─────────┘┴
doc └───────────┘ └─┘ └───┘ ┴ └────┘ └────┘ ┴
txt └───┘ ┴ └────┘ └────┘ ┴
par └───┘ ┴ └────┘ └────┘ ┴
pid └┘ ┴ ┴ └────┘ ┴
st └─────────────────────┘┴└───────────────────────────────┘
549 have sum.inr ⁻¹' (sum.inl '' s : set (α ⊕ β)) = ∅ :=
id └─────┘ └─┘ └─────┘ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─┘ └─────┘ └┘ └─┘ ┴ ┴ ┴
typ └─────┘ └─┘ └─────┘ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc └─┘
550 eq_empty_of_subset_empty $ assume x ⟨y, hy, eq⟩, by contradiction,
id └──────────────────────┘ ┴ ┴
src └──────────────────────┘ └───────────┘
typ └──────────────────────┘ ┴ ┴ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
st └────────────┘
551 show is_measurable (sum.inr ⁻¹' _), by rw [this]; exact is_measurable.empty⟩
id └───────────┘ └─────┘ └─┘ └──┘ └─────────────────┘
src └───────────┘ └─────┘ └─┘ └──┘ ┴ └────┘└─────────────────┘
typ └───────────┘ └─────┘ └─┘ └──┘└──┘┴ └────┘└─────────────────┘
doc └───────────┘ └─┘ └──┘ ┴ └────┘
txt └──┘ ┴ └────┘
par └──┘ ┴ └────┘
pid └┘ ┴ ┴
st └───────┘┴└─────────────────────────┘
552
553 lemma is_measurable_range_inl : is_measurable (range sum.inl : set (α ⊕ β)) :=
id └───────────┘ └───┘ └─────┘ └─┘ ┴ ┴ ┴
src └───────────┘ └───┘ └─────┘ └─┘ ┴
typ └───────────┘ └───┘ └─────┘ └─┘ ┴ ┴ ┴
doc └───────────┘ └───┘
554 by rw [← image_univ]; exact is_measurable_inl_image is_measurable.univ
id └────────┘ └─────────────────────┘ └────────────────┘
src └────┘└────────┘┴ └────┘└─────────────────────┘┴└────────────────┘└
typ └────┘└────────┘┴ └────┘└─────────────────────┘┴└────────────────┘└
doc └────┘ ┴ └────┘ ┴ └
txt └────┘ ┴ └────┘ ┴ └
par └────┘ ┴ └────┘ ┴ └
pid └──┘ ┴ ┴ ┴ └
st └───────────────┘┴└──────────────────────────────────────────────────
555
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
556 lemma is_measurable_inr_image {s : set β} (hs : is_measurable s) :
id └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
557 is_measurable (sum.inr '' s : set (α ⊕ β)) :=
id └───────────┘ └─────┘ └┘ ┴ └─┘ ┴ ┴ ┴
src └───────────┘ └─────┘ └┘ └─┘ ┴
typ └───────────┘ └─────┘ └┘ ┴ └─┘ ┴ ┴ ┴
doc └───────────┘
558 ⟨ have sum.inl ⁻¹' (sum.inr '' s : set (α ⊕ β)) = ∅ :=
id └─────┘ └─┘ └─────┘ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─┘ └─────┘ └┘ └─┘ ┴ ┴ ┴
typ └─────┘ └─┘ └─────┘ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc └─┘
559 eq_empty_of_subset_empty $ assume x ⟨y, hy, eq⟩, by contradiction,
id └──────────────────────┘ ┴ ┴
src └──────────────────────┘ └───────────┘
typ └──────────────────────┘ ┴ ┴ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
st └────────────┘
560 show is_measurable (sum.inl ⁻¹' _), by rw [this]; exact is_measurable.empty,
id └───────────┘ └─────┘ └─┘ └──┘ └─────────────────┘
src └───────────┘ └─────┘ └─┘ └──┘ ┴ └────┘└─────────────────┘
typ └───────────┘ └─────┘ └─┘ └──┘└──┘┴ └────┘└─────────────────┘
doc └───────────┘ └─┘ └──┘ ┴ └────┘
txt └──┘ ┴ └────┘
par └──┘ ┴ └────┘
pid └┘ ┴ ┴
st └───────┘┴└─────────────────────────┘
561 show is_measurable (sum.inr ⁻¹' _), by rwa [preimage_image_eq]; exact (assume a b, sum.inr.inj)⟩
id └───────────┘ └─────┘ └─┘ └───────────────┘ └─────────┘
src └───────────┘ └─────┘ └─┘ └───┘└───────────────┘┴ └────┘ └────┘└─────────┘┴
typ └───────────┘ └─────┘ └─┘ └───┘└───────────────┘┴ └────┘ └────┘└─────────┘┴
doc └───────────┘ └─┘ └───┘ ┴ └────┘ └────┘ ┴
txt └───┘ ┴ └────┘ └────┘ ┴
par └───┘ ┴ └────┘ └────┘ ┴
pid └┘ ┴ ┴ └────┘ ┴
st └─────────────────────┘┴└───────────────────────────────┘
562
563 lemma is_measurable_range_inr : is_measurable (range sum.inr : set (α ⊕ β)) :=
id └───────────┘ └───┘ └─────┘ └─┘ ┴ ┴ ┴
src └───────────┘ └───┘ └─────┘ └─┘ ┴
typ └───────────┘ └───┘ └─────┘ └─┘ ┴ ┴ ┴
doc └───────────┘ └───┘
564 by rw [← image_univ]; exact is_measurable_inr_image is_measurable.univ
id └────────┘ └─────────────────────┘ └────────────────┘
src └────┘└────────┘┴ └────┘└─────────────────────┘┴└────────────────┘└
typ └────┘└────────┘┴ └────┘└─────────────────────┘┴└────────────────┘└
doc └────┘ ┴ └────┘ ┴ └
txt └────┘ ┴ └────┘ ┴ └
par └────┘ ┴ └────┘ ┴ └
pid └──┘ ┴ ┴ ┴ └
st └───────────────┘┴└──────────────────────────────────────────────────
565
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
566 end sum
567
568 instance {β : α → Type v} [m : Πa, measurable_space (β a)] : measurable_space (sigma β) :=
id ┴ ┴ └──────────────┘ ┴ ┴ └──────────────┘ └───┘ ┴
src └──────────────┘ └──────────────┘ └───┘
typ ┴ ┴ └──────────────┘ ┴ ┴ └──────────────┘ └───┘ ┴
569 ⨅a, (m a).map (sigma.mk a)
id ┴┴┴ ┴ ┴ └─┘ └──────┘ ┴
src ┴ ┴ └─┘ └──────┘
typ ┴┴┴ ┴ ┴ └─┘ └──────┘ ┴
doc ┴ ┴ └─┘
570
571 end constructions
572
573 /-- Equivalences between measurable spaces. Main application is the simplification of measurability
574 statements along measurable equivalences. -/
575 structure measurable_equiv (α β : Type*) [measurable_space α] [measurable_space β] extends α ≃ β :=
id └───┘ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴
src └──────────────┘ └──────────────┘ ┴
typ └───┘ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴
doc ┴
576 (measurable_to_fun : measurable to_fun)
id └────────┘ └────┘
src └────────┘
typ └────────┘ └────┘
doc └────────┘
577 (measurable_inv_fun : measurable inv_fun)
id └────────┘ └─────┘
src └────────┘
typ └────────┘ └─────┘
doc └────────┘
578
579
580 namespace measurable_equiv
581
582 instance (α β) [measurable_space α] [measurable_space β] : has_coe_to_fun (measurable_equiv α β) :=
id └──────────────┘ ┴ └──────────────┘ ┴ └────────────┘ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘ └────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └────────────┘ └──────────────┘ ┴ ┴
doc └──────────────┘
583 ⟨λ_, α → β, λe, e.to_equiv⟩
id ┴ ┴ ┴ ┴ ┴└───────┘
src └───────┘
typ ┴ ┴ ┴ ┴ ┴└───────┘
584
585 lemma coe_eq {α β} [measurable_space α] [measurable_space β] (e : measurable_equiv α β) :
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
586 (e : α → β) = e.to_equiv := rfl
id ┴ ┴ ┴ ┴ ┴└───────┘ └─┘
src ┴ └───────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴└───────┘ └─┘
587
588 def refl (α : Type*) [measurable_space α] : measurable_equiv α α :=
id └──────────────┘ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
589 { to_equiv := equiv.refl α,
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
590 measurable_to_fun := measurable_id, measurable_inv_fun := measurable_id }
id └───────────┘ └───────────┘
src └───────────┘ └───────────┘
typ └───────────┘ └───────────┘
591
592 def trans [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
593 (ab : measurable_equiv α β) (bc : measurable_equiv β γ) :
id └──────────────┘ ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘ └──────────────┘
594 measurable_equiv α γ :=
id └──────────────┘ ┴ ┴
src └──────────────┘
typ └──────────────┘ ┴ ┴
doc └──────────────┘
595 { to_equiv := ab.to_equiv.trans bc.to_equiv,
id └┘└───────┘└────┘ └┘└───────┘
src └───────┘└────┘ └───────┘
typ └┘└───────┘└────┘ └┘└───────┘
596 measurable_to_fun := bc.measurable_to_fun.comp ab.measurable_to_fun,
id └┘└────────────────┘└───┘ └┘└────────────────┘
src └────────────────┘└───┘ └────────────────┘
typ └┘└────────────────┘└───┘ └┘└────────────────┘
597 measurable_inv_fun := ab.measurable_inv_fun.comp bc.measurable_inv_fun }
id └┘└─────────────────┘└───┘ └┘└─────────────────┘
src └─────────────────┘└───┘ └─────────────────┘
typ └┘└─────────────────┘└───┘ └┘└─────────────────┘
598
599 lemma trans_to_equiv {α β} [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
600 (e : measurable_equiv α β) (f : measurable_equiv β γ) :
id └──────────────┘ ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘ └──────────────┘
601 (e.trans f).to_equiv = e.to_equiv.trans f.to_equiv := rfl
id ┴└────┘ ┴ └──────┘ ┴ ┴└───────┘└────┘ ┴└───────┘ └─┘
src └────┘ └──────┘ ┴ └───────┘└────┘ └───────┘ └─┘
typ ┴└────┘ ┴ └──────┘ ┴ ┴└───────┘└────┘ ┴└───────┘ └─┘
602
603 def symm [measurable_space α] [measurable_space β] (ab : measurable_equiv α β) :
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
604 measurable_equiv β α :=
id └──────────────┘ ┴ ┴
src └──────────────┘
typ └──────────────┘ ┴ ┴
doc └──────────────┘
605 { to_equiv := ab.to_equiv.symm,
id └┘└───────┘└───┘
src └───────┘└───┘
typ └┘└───────┘└───┘
606 measurable_to_fun := ab.measurable_inv_fun,
id └┘└─────────────────┘
src └─────────────────┘
typ └┘└─────────────────┘
607 measurable_inv_fun := ab.measurable_to_fun }
id └┘└────────────────┘
src └────────────────┘
typ └┘└────────────────┘
608
609 lemma symm_to_equiv {α β} [measurable_space α] [measurable_space β] (e : measurable_equiv α β) :
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
610 e.symm.to_equiv = e.to_equiv.symm := rfl
id ┴└───┘└───────┘ ┴ ┴└───────┘└───┘ └─┘
src └───┘└───────┘ ┴ └───────┘└───┘ └─┘
typ ┴└───┘└───────┘ ┴ ┴└───────┘└───┘ └─┘
611
612 protected def cast {α β} [i₁ : measurable_space α] [i₂ : measurable_space β]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
613 (h : α = β) (hi : i₁ == i₂) : measurable_equiv α β :=
id ┴ ┴ ┴ └┘ └┘ └┘ └──────────────┘ ┴ ┴
src ┴ └┘ └──────────────┘
typ ┴ ┴ ┴ └┘ └┘ └┘ └──────────────┘ ┴ ┴
doc └──────────────┘
614 { to_equiv := equiv.cast h,
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
615 measurable_to_fun := by unfreezeI; subst h; subst hi; exact measurable_id,
id ┴ └┘ └───────────┘
src └───────┘ └────┘ └────┘ └────┘└───────────┘
typ └───────┘ └────┘┴ └────┘└┘ └────┘└───────────┘
doc └───────┘ └────┘ └────┘ └────┘
txt └───────┘ └────┘ └────┘ └────┘
par └───────┘ └────┘ └────┘ └────┘
pid ┴ ┴ ┴
st └────────────────────────────────────────────────┘
616 measurable_inv_fun := by unfreezeI; subst h; subst hi; exact measurable_id }
id ┴ └┘ └───────────┘
src └───────┘ └────┘ └────┘ └────┘└───────────┘┴
typ └───────┘ └────┘┴ └────┘└┘ └────┘└───────────┘┴
doc └───────┘ └────┘ └────┘ └────┘ ┴
txt └───────┘ └────┘ └────┘ └────┘ ┴
par └───────┘ └────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴
st └─────────────────────────────────────────────────┘
617
618 protected lemma measurable {α β} [measurable_space α] [measurable_space β]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
619 (e : measurable_equiv α β) : measurable (e : α → β) :=
id └──────────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴
src └──────────────┘ └────────┘
typ └──────────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └──────────────┘ └────────┘
620 e.measurable_to_fun
id ┴└────────────────┘
src └────────────────┘
typ ┴└────────────────┘
621
622 protected lemma measurable_coe_iff {α β γ} [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
623 {f : β → γ} (e : measurable_equiv α β) : measurable (f ∘ e) ↔ measurable f :=
id ┴ ┴ └──────────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
src └──────────────┘ └────────┘ ┴ ┴ └────────┘
typ ┴ ┴ └──────────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └──────────────┘ └────────┘ └────────┘
624 iff.intro
id └───────┘
src └───────┘
typ └───────┘
625 (assume hfe,
id └─┘
typ └─┘
626 have measurable (f ∘ (e.symm.trans e).to_equiv) := hfe.comp e.symm.measurable,
id └────────┘ ┴ ┴ ┴└───┘└────┘ ┴ └──────┘ └─┘└───┘ ┴└───┘└─────────┘
src └────────┘ ┴ └───┘└────┘ └──────┘ └───┘ └───┘└─────────┘
typ └────────┘ ┴ ┴ ┴└───┘└────┘ ┴ └──────┘ └─┘└───┘ ┴└───┘└─────────┘
doc └────────┘
627 by rwa [trans_to_equiv, symm_to_equiv, equiv.symm_trans] at this)
id └────────────┘ └───────────┘ └──────────────┘
src └───┘└────────────┘└┘└───────────┘└┘└──────────────┘└───────┘
typ └───┘└────────────┘└┘└───────────┘└┘└──────────────┘└───────┘
doc └───┘ └┘ └┘ └───────┘
txt └───┘ └┘ └┘ └───────┘
par └───┘ └┘ └┘ └───────┘
pid └┘ └┘ └┘ ┴└──────┘
st └──────────────────┘└─────────────┘└────────────────┘┴└──────┘
628 (λh, h.comp e.measurable)
id ┴ ┴└───┘ ┴└─────────┘
src └───┘ └─────────┘
typ ┴ ┴└───┘ ┴└─────────┘
629
630 def prod_congr [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
631 (ab : measurable_equiv α β) (cd : measurable_equiv γ δ) :
id └──────────────┘ ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘ └──────────────┘
632 measurable_equiv (α × γ) (β × δ) :=
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────────┘
633 { to_equiv := equiv.prod_congr ab.to_equiv cd.to_equiv,
id └──────────────┘ └┘└───────┘ └┘└───────┘
src └──────────────┘ └───────┘ └───────┘
typ └──────────────┘ └┘└───────┘ └┘└───────┘
634 measurable_to_fun := measurable.prod_mk
id └────────────────┘
src └────────────────┘
typ └────────────────┘
635 (ab.measurable_to_fun.comp (measurable.fst measurable_id))
id └┘└────────────────┘└───┘ └────────────┘ └───────────┘
src └────────────────┘└───┘ └────────────┘ └───────────┘
typ └┘└────────────────┘└───┘ └────────────┘ └───────────┘
636 (cd.measurable_to_fun.comp (measurable.snd measurable_id)),
id └┘└────────────────┘└───┘ └────────────┘ └───────────┘
src └────────────────┘└───┘ └────────────┘ └───────────┘
typ └┘└────────────────┘└───┘ └────────────┘ └───────────┘
637 measurable_inv_fun := measurable.prod_mk
id └────────────────┘
src └────────────────┘
typ └────────────────┘
638 (ab.measurable_inv_fun.comp (measurable.fst measurable_id))
id └┘└─────────────────┘└───┘ └────────────┘ └───────────┘
src └─────────────────┘└───┘ └────────────┘ └───────────┘
typ └┘└─────────────────┘└───┘ └────────────┘ └───────────┘
639 (cd.measurable_inv_fun.comp (measurable.snd measurable_id)) }
id └┘└─────────────────┘└───┘ └────────────┘ └───────────┘
src └─────────────────┘└───┘ └────────────┘ └───────────┘
typ └┘└─────────────────┘└───┘ └────────────┘ └───────────┘
640
641 def prod_comm [measurable_space α] [measurable_space β] : measurable_equiv (α × β) (β × α) :=
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ └──────────────┘ └──────────────┘ ┴ ┴
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────────┘
642 { to_equiv := equiv.prod_comm α β,
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
643 measurable_to_fun := measurable.prod_mk (measurable.snd measurable_id) (measurable.fst measurable_id),
id └────────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
src └────────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
typ └────────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
644 measurable_inv_fun := measurable.prod_mk (measurable.snd measurable_id) (measurable.fst measurable_id) }
id └────────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
src └────────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
typ └────────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
645
646 def sum_congr [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ]
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
647 (ab : measurable_equiv α β) (cd : measurable_equiv γ δ) :
id └──────────────┘ ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘ └──────────────┘
648 measurable_equiv (α ⊕ γ) (β ⊕ δ) :=
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────────┘
649 { to_equiv := equiv.sum_congr ab.to_equiv cd.to_equiv,
id └─────────────┘ └┘└───────┘ └┘└───────┘
src └─────────────┘ └───────┘ └───────┘
typ └─────────────┘ └┘└───────┘ └┘└───────┘
650 measurable_to_fun :=
651 begin
st └─────
652 cases ab with ab' abm, cases ab', cases cd with cd' cdm, cases cd',
id └┘ └─┘ └┘ └─┘
src └────┘ └───────────┘ └────┘ └────┘ └───────────┘ └────┘
typ └────┘└┘└───────────┘ └────┘└─┘ └────┘└┘└───────────┘ └────┘└─┘
doc └────┘ └───────────┘ └────┘ └────┘ └───────────┘ └────┘
txt └────┘ └───────────┘ └────┘ └────┘ └───────────┘ └────┘
par └────┘ └───────────┘ └────┘ └────┘ └───────────┘ └────┘
pid ┴ └───────────┘ ┴ ┴ └───────────┘ ┴
st ──────────────────────────┘└─────────┘└─────────────────────┘└─────────┘└─
653 refine measurable_sum (measurable_inl.comp abm) (measurable_inr.comp cdm)
id └────────────┘ └─────────────────┘ └─┘ └─────────────────┘ └─┘
src └─────┘└────────────┘┴ └─────────────────┘┴ └┘ └─────────────────┘┴ └─
typ └─────┘└────────────┘┴ └─────────────────┘┴└─┘└┘ └─────────────────┘┴└─┘└─
doc └─────┘ ┴ ┴ └┘ ┴ └─
txt └─────┘ ┴ ┴ └┘ ┴ └─
par └─────┘ ┴ ┴ └┘ ┴ └─
pid ┴ ┴ ┴ └┘ ┴ ┴└
st ────────────────────────────────────────────────────────────────────────────────
654 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
655 measurable_inv_fun :=
656 begin
st └─────
657 cases ab with ab' _ abm, cases ab', cases cd with cd' _ cdm, cases cd',
id └┘ └─┘ └┘ └─┘
src └────┘ └─────────────┘ └────┘ └────┘ └─────────────┘ └────┘
typ └────┘└┘└─────────────┘ └────┘└─┘ └────┘└┘└─────────────┘ └────┘└─┘
doc └────┘ └─────────────┘ └────┘ └────┘ └─────────────┘ └────┘
txt └────┘ └─────────────┘ └────┘ └────┘ └─────────────┘ └────┘
par └────┘ └─────────────┘ └────┘ └────┘ └─────────────┘ └────┘
pid ┴ └─────────────┘ ┴ ┴ └─────────────┘ ┴
st ────────────────────────────┘└─────────┘└───────────────────────┘└─────────┘└─
658 refine measurable_sum (measurable_inl.comp abm) (measurable_inr.comp cdm)
id └────────────┘ └─────────────────┘ └─┘ └─────────────────┘ └─┘
src └─────┘└────────────┘┴ └─────────────────┘┴ └┘ └─────────────────┘┴ └─
typ └─────┘└────────────┘┴ └─────────────────┘┴└─┘└┘ └─────────────────┘┴└─┘└─
doc └─────┘ ┴ ┴ └┘ ┴ └─
txt └─────┘ ┴ ┴ └┘ ┴ └─
par └─────┘ ┴ ┴ └┘ ┴ └─
pid ┴ ┴ ┴ └┘ ┴ ┴└
st ────────────────────────────────────────────────────────────────────────────────
659 end }
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
660
661 def set.prod [measurable_space α] [measurable_space β] (s : set α) (t : set β) :
id └──────────────┘ ┴ └──────────────┘ ┴ └─┘ ┴ └─┘ ┴
src └──────────────┘ └──────────────┘ └─┘ └─┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └─┘ ┴ └─┘ ┴
662 measurable_equiv (set.prod s t) (s × t) :=
id └──────────────┘ └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ └──────┘ ┴
typ └──────────────┘ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────────────┘ └──────┘
663 { to_equiv := equiv.set.prod s t,
id └────────────┘ ┴ ┴
src └────────────┘
typ └────────────┘ ┴ ┴
664 measurable_to_fun := measurable.prod_mk
id └────────────────┘
src └────────────────┘
typ └────────────────┘
665 (measurable.subtype_mk $ measurable.fst $ measurable.subtype_val $ measurable_id)
id └───────────────────┘ └────────────┘ └────────────────────┘ └───────────┘
src └───────────────────┘ └────────────┘ └────────────────────┘ └───────────┘
typ └───────────────────┘ └────────────┘ └────────────────────┘ └───────────┘
666 (measurable.subtype_mk $ measurable.snd $ measurable.subtype_val $ measurable_id),
id └───────────────────┘ └────────────┘ └────────────────────┘ └───────────┘
src └───────────────────┘ └────────────┘ └────────────────────┘ └───────────┘
typ └───────────────────┘ └────────────┘ └────────────────────┘ └───────────┘
667 measurable_inv_fun := measurable.subtype_mk $ measurable.prod_mk
id └───────────────────┘ └────────────────┘
src └───────────────────┘ └────────────────┘
typ └───────────────────┘ └────────────────┘
668 (measurable.subtype_val $ measurable.fst $ measurable_id)
id └────────────────────┘ └────────────┘ └───────────┘
src └────────────────────┘ └────────────┘ └───────────┘
typ └────────────────────┘ └────────────┘ └───────────┘
669 (measurable.subtype_val $ measurable.snd $ measurable_id) }
id └────────────────────┘ └────────────┘ └───────────┘
src └────────────────────┘ └────────────┘ └───────────┘
typ └────────────────────┘ └────────────┘ └───────────┘
670
671 def set.univ (α : Type*) [measurable_space α] : measurable_equiv (univ : set α) α :=
id └──────────────┘ ┴ └──────────────┘ └──┘ └─┘ ┴ ┴
src └──────────────┘ └──────────────┘ └──┘ └─┘
typ └──────────────┘ ┴ └──────────────┘ └──┘ └─┘ ┴ ┴
doc └──────────────┘
672 { to_equiv := equiv.set.univ α,
id └────────────┘ ┴
src └────────────┘
typ └────────────┘ ┴
673 measurable_to_fun := measurable.subtype_val measurable_id,
id └────────────────────┘ └───────────┘
src └────────────────────┘ └───────────┘
typ └────────────────────┘ └───────────┘
674 measurable_inv_fun := measurable.subtype_mk measurable_id }
id └───────────────────┘ └───────────┘
src └───────────────────┘ └───────────┘
typ └───────────────────┘ └───────────┘
675
676 def set.singleton [measurable_space α] (a:α) : measurable_equiv ({a} : set α) unit :=
id └──────────────┘ ┴ ┴ └──────────────┘ ┴┴ └─┘ ┴ └──┘
src └──────────────┘ └──────────────┘ ┴ └─┘ └──┘
typ └──────────────┘ ┴ ┴ └──────────────┘ ┴┴ └─┘ ┴ └──┘
doc └──────────────┘ └──┘
677 { to_equiv := equiv.set.singleton a,
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
678 measurable_to_fun := measurable_const,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
679 measurable_inv_fun := measurable.subtype_mk $ show measurable (λu:unit, a), from
id └───────────────────┘ └────────┘ └──┘ ┴
src └───────────────────┘ └────────┘ └──┘
typ └───────────────────┘ └────────┘ └──┘ ┴
doc └────────┘ └──┘
680 measurable_const }
id └──────────────┘
src └──────────────┘
typ └──────────────┘
681
682 noncomputable def set.image [measurable_space α] [measurable_space β]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
683 (f : α → β) (s : set α)
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
684 (hf : function.injective f)
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
685 (hfm : measurable f) (hfi : ∀s, is_measurable s → is_measurable (f '' s)) :
id └────────┘ ┴ ┴ └───────────┘ ┴ └───────────┘ ┴ └┘ ┴
src └────────┘ └───────────┘ └───────────┘ └┘
typ └────────┘ ┴ ┴ └───────────┘ ┴ └───────────┘ ┴ └┘ ┴
doc └────────┘ └───────────┘ └───────────┘
686 measurable_equiv s (f '' s) :=
id └──────────────┘ ┴ ┴ └┘ ┴
src └──────────────┘ └┘
typ └──────────────┘ ┴ ┴ └┘ ┴
doc └──────────────┘
687 { to_equiv := equiv.set.image f s hf,
id └─────────────┘ ┴ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ ┴ └┘
688 measurable_to_fun :=
689 begin
st └─────
690 have : measurable (λa:s, f a) := hfm.comp (measurable.subtype_val measurable_id),
id └────────┘ ┴ ┴ └──────┘ └────────────────────┘ └───────────┘
src └─────┘└────────┘┴ └┘ └┘ ┴ └───┘└──────┘┴ └────────────────────┘┴└───────────┘┴
typ └─────┘└────────┘┴ └┘┴└┘┴┴ └───┘└──────┘┴ └────────────────────┘┴└───────────┘┴
doc └─────┘└────────┘┴ └┘ └┘ ┴ └───┘ ┴ ┴ ┴
txt └─────┘ ┴ └┘ └┘ ┴ └───┘ ┴ ┴ ┴
par └─────┘ ┴ └┘ └┘ ┴ └───┘ ┴ ┴ ┴
pid └───┘└┘ ┴ └┘ └┘ ┴ ┴└──┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
691 refine measurable.subtype_mk _,
id └───────────────────┘
src └─────┘└───────────────────┘└┘
typ └─────┘└───────────────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ─────────────────────────────────┘└─
692 convert this,
id └──┘
src └──────┘
typ └──────┘└──┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ───────────────┘└─
693 ext ⟨a, h⟩, refl
src └────────┘ └────
typ └────────┘ └────
doc └────────┘ └────
txt └────────┘ └────
par └────────┘ └────
pid └─────┘ └
st ─────────────┘└──────
694 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
695 measurable_inv_fun :=
696 assume t ⟨u, (hu : is_measurable u), eq⟩,
id ┴ ┴ └───────────┘
src └───────────┘
typ ┴ ┴ └───────────┘
doc └───────────┘
697 begin
st └─────
698 clear_, subst eq,
id └┘
src └────┘ └────┘└┘
typ └────┘ └────┘└┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴
st ───────────┘└────────┘└─
699 show is_measurable {x : f '' s | ((equiv.set.image f s hf).inv_fun x).val ∈ u},
id └───────────┘ ┴ └┘ └─────────────┘ ┴ ┴ └┘ ┴ ┴
src └───┘└───────────┘┴┴└──┘ ┴└┘┴ └─┘ └─────────────┘┴ ┴ ┴ └────────┘ └────┘┴┴ ┴
typ └───┘└───────────┘┴┴└──┘ ┴└┘┴ └─┘ └─────────────┘┴┴┴┴┴└┘└────────┘ └────┘┴┴┴┴
doc └───┘└───────────┘┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────┘ └────┘ ┴ ┴
txt └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────┘ └────┘ ┴ ┴
par └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────┘ └────┘ ┴ ┴
pid └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────┘ └────┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
700 have : ∀(a ∈ s) (h : ∃a', a' ∈ s ∧ a' = a), classical.some h = a :=
id ┴ ┴ ┴ ┴ └────────────┘
src └─────┘ └───┘ └─────┘┴└┘┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴└────────────┘┴ ┴ ┴ └───
typ └─────┘ └───┘ └─────┘┴└┘┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴└────────────┘┴ ┴ ┴ └───
doc └─────┘ └───┘ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
txt └─────┘ └───┘ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └─────┘ └───┘ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid └───┘└┘ └───┘ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────────────────
701 λa ha h, (classical.some_spec h).2,
id └─────────────────┘
src ───────┘ └──────┘ └─────────────────┘┴ └─┘
typ ───────┘ └──────┘ └─────────────────┘┴ └─┘
doc ───────┘ └──────┘ ┴ └─┘
txt ───────┘ └──────┘ ┴ └─┘
par ───────┘ └──────┘ ┴ └─┘
pid ───────┘ └──────┘ ┴ ┴└┘
st ─────────────────────────────────────────┘└─
702 rw show {x:f '' s | ((equiv.set.image f s hf).inv_fun x).val ∈ u} = subtype.val ⁻¹' (f '' u),
id ┴ └─────────────┘ ┴ └┘ ┴ └─────────┘ └─┘ ┴ ┴
src └─┘ ┴┴└┘ ┴ ┴ └─┘ └─────────────┘┴ ┴ ┴ └────────┘ └────┘ ┴ └┘ ┴└─────────┘┴└─┘┴ ┴ ┴ └──
typ └─┘ ┴┴└┘ ┴ ┴ └─┘ └─────────────┘┴ ┴┴┴└┘└────────┘ └────┘ ┴ └┘┴┴└─────────┘┴└─┘┴ ┴┴ ┴┴└──
doc └─┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────┘ └────┘ ┴ └┘ ┴ ┴└─┘┴ ┴ ┴ └──
txt └─┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────┘ └────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──
par └─┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────┘ └────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──
pid ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────┘ └────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──
st ────────────────────────────────────────────────────────────────────────────────────────────────────
703 by ext ⟨b, a, hbs, rfl⟩; simp [equiv.set.image, equiv.set.image_of_inj_on, hf, this _ hbs],
id └─────────────┘ └───────────────────────┘ └┘ └──┘ └─┘
src ──────────┘└──────────────────┘└┘└────┘└─────────────┘└┘└───────────────────────┘└┘ └┘ └─┘ ┴
typ ──────────┘└──────────────────┘└┘└────┘└─────────────┘└┘└───────────────────────┘└┘└┘└┘└──┘└─┘└─┘┴
doc ──────────┘└──────────────────┘└┘└────┘ └┘ └┘ └┘ └─┘ ┴
txt ──────────┘└──────────────────┘└┘└────┘ └┘ └┘ └┘ └─┘ ┴
par ──────────┘└──────────────────┘└┘└────┘ └┘ └┘ └┘ └─┘ ┴
pid ──────────────────────────────────────┘ └┘ └┘ └┘ └─┘ ┴
st ─────────┘└──────────────────────────────────────────────────────────────────────────────────────┘└─
704 exact (measurable.subtype_val measurable_id) (f '' u) (hfi u hu)
id └────────────────────┘ └───────────┘ ┴ └─┘ ┴ └┘
src └────┘ └────────────────────┘┴└───────────┘└┘ ┴ ┴ └┘ ┴ ┴ └─
typ └────┘ └────────────────────┘┴└───────────┘└┘ ┴┴ ┴ └┘ └─┘┴┴┴└┘└─
doc └────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─
txt └────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─
par └────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─
pid ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴└
st ───────────────────────────────────────────────────────────────────────
705 end }
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
706
707 noncomputable def set.range [measurable_space α] [measurable_space β]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
708 (f : α → β) (hf : function.injective f) (hfm : measurable f)
id ┴ ┴ └────────────────┘ ┴ └────────┘ ┴
src └────────────────┘ └────────┘
typ ┴ ┴ └────────────────┘ ┴ └────────┘ ┴
doc └────────┘
709 (hfi : ∀s, is_measurable s → is_measurable (f '' s)) :
id ┴ └───────────┘ ┴ └───────────┘ ┴ └┘ ┴
src └───────────┘ └───────────┘ └┘
typ ┴ └───────────┘ ┴ └───────────┘ ┴ └┘ ┴
doc └───────────┘ └───────────┘
710 measurable_equiv α (range f) :=
id └──────────────┘ ┴ └───┘ ┴
src └──────────────┘ └───┘
typ └──────────────┘ ┴ └───┘ ┴
doc └──────────────┘ └───┘
711 (measurable_equiv.set.univ _).symm.trans $
id └───────────────────────┘ └──┘ └───┘
src └───────────────────────┘ └──┘ └───┘
typ └───────────────────────┘ └──┘ └───┘
712 (measurable_equiv.set.image f univ hf hfm hfi).trans $
id └────────────────────────┘ ┴ └──┘ └┘ └─┘ └─┘ └───┘
src └────────────────────────┘ └──┘ └───┘
typ └────────────────────────┘ ┴ └──┘ └┘ └─┘ └─┘ └───┘
713 measurable_equiv.cast (by rw image_univ) (by rw image_univ)
id └───────────────────┘ └────────┘ └────────┘
src └───────────────────┘ └─┘└────────┘ └─┘└────────┘
typ └───────────────────┘ └─┘└────────┘ └─┘└────────┘
doc └─┘ └─┘
txt └─┘ └─┘
par └─┘ └─┘
pid ┴ ┴
st └────────────┘ └────────────┘
714
715 def set.range_inl [measurable_space α] [measurable_space β] :
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
716 measurable_equiv (range sum.inl : set (α ⊕ β)) α :=
id └──────────────┘ └───┘ └─────┘ └─┘ ┴ ┴ ┴ ┴
src └──────────────┘ └───┘ └─────┘ └─┘ ┴
typ └──────────────┘ └───┘ └─────┘ └─┘ ┴ ┴ ┴ ┴
doc └──────────────┘ └───┘
717 { to_fun := λab, match ab with
id └┘ └┘
typ └┘ └┘
718 | ⟨sum.inl a, _⟩ := a
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
719 | ⟨sum.inr b, p⟩ := have false, by cases p; contradiction, this.elim
id └─────┘ └───┘ ┴ └──┘└───┘
src └─────┘ └───┘ └────┘ └───────────┘ └───┘
typ └─────┘ └───┘ └────┘┴ └───────────┘ └──┘└───┘
doc └────┘ └───────────┘
txt └────┘ └───────────┘
par └────┘ └───────────┘
pid ┴
st └─────────────────────┘
720 end,
721 inv_fun := λa, ⟨sum.inl a, a, rfl⟩,
id ┴ └─────┘ ┴ ┴ └─┘
src └─────┘ └─┘
typ ┴ └─────┘ ┴ ┴ └─┘
722 left_inv := assume ⟨ab, a, eq⟩, by subst eq; refl,
id ┴ └┘
src └────┘└┘ └──┘
typ ┴ └────┘└┘ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └─────────────┘
723 right_inv := assume a, rfl,
id ┴ └─┘
src └─┘
typ ┴ └─┘
724 measurable_to_fun := assume s (hs : is_measurable s),
id ┴ └───────────┘ ┴
src └───────────┘
typ ┴ └───────────┘ ┴
doc └───────────┘
725 begin
st └─────
726 refine ⟨_, is_measurable_inl_image hs, set.ext _⟩,
id └─────────────────────┘ └┘ └─────┘
src └─────┘ └─┘└─────────────────────┘┴ └┘└─────┘└─┘
typ └─────┘ └─┘└─────────────────────┘┴└┘└┘└─────┘└─┘
doc └─────┘ └─┘ ┴ └┘ └─┘
txt └─────┘ └─┘ ┴ └┘ └─┘
par └─────┘ └─┘ ┴ └┘ └─┘
pid ┴ └─┘ ┴ └┘ └─┘
st ──────────────────────────────────────────────────────┘└─
727 rintros ⟨ab, a, rfl⟩,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └───────────┘
st ─────────────────────────┘└─
728 simp [set.range_inl._match_1]
id └────────────────────┘
src └────┘ └─
typ └────┘└────────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st ────────────────────────────────────
729 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
730 measurable_inv_fun := measurable.subtype_mk measurable_inl }
id └───────────────────┘ └────────────┘
src └───────────────────┘ └────────────┘
typ └───────────────────┘ └────────────┘
731
732 def set.range_inr [measurable_space α] [measurable_space β] :
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
733 measurable_equiv (range sum.inr : set (α ⊕ β)) β :=
id └──────────────┘ └───┘ └─────┘ └─┘ ┴ ┴ ┴ ┴
src └──────────────┘ └───┘ └─────┘ └─┘ ┴
typ └──────────────┘ └───┘ └─────┘ └─┘ ┴ ┴ ┴ ┴
doc └──────────────┘ └───┘
734 { to_fun := λab, match ab with
id └┘ └┘
typ └┘ └┘
735 | ⟨sum.inr b, _⟩ := b
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
736 | ⟨sum.inl a, p⟩ := have false, by cases p; contradiction, this.elim
id └─────┘ └───┘ ┴ └──┘└───┘
src └─────┘ └───┘ └────┘ └───────────┘ └───┘
typ └─────┘ └───┘ └────┘┴ └───────────┘ └──┘└───┘
doc └────┘ └───────────┘
txt └────┘ └───────────┘
par └────┘ └───────────┘
pid ┴
st └─────────────────────┘
737 end,
738 inv_fun := λb, ⟨sum.inr b, b, rfl⟩,
id ┴ └─────┘ ┴ ┴ └─┘
src └─────┘ └─┘
typ ┴ └─────┘ ┴ ┴ └─┘
739 left_inv := assume ⟨ab, b, eq⟩, by subst eq; refl,
id ┴ └┘
src └────┘└┘ └──┘
typ ┴ └────┘└┘ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └─────────────┘
740 right_inv := assume b, rfl,
id ┴ └─┘
src └─┘
typ ┴ └─┘
741 measurable_to_fun := assume s (hs : is_measurable s),
id ┴ └───────────┘ ┴
src └───────────┘
typ ┴ └───────────┘ ┴
doc └───────────┘
742 begin
st └─────
743 refine ⟨_, is_measurable_inr_image hs, set.ext _⟩,
id └─────────────────────┘ └┘ └─────┘
src └─────┘ └─┘└─────────────────────┘┴ └┘└─────┘└─┘
typ └─────┘ └─┘└─────────────────────┘┴└┘└┘└─────┘└─┘
doc └─────┘ └─┘ ┴ └┘ └─┘
txt └─────┘ └─┘ ┴ └┘ └─┘
par └─────┘ └─┘ ┴ └┘ └─┘
pid ┴ └─┘ ┴ └┘ └─┘
st ──────────────────────────────────────────────────────┘└─
744 rintros ⟨ab, b, rfl⟩,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └───────────┘
st ─────────────────────────┘└─
745 simp [set.range_inr._match_1]
id └────────────────────┘
src └────┘ └─
typ └────┘└────────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st ────────────────────────────────────
746 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
747 measurable_inv_fun := measurable.subtype_mk measurable_inr }
id └───────────────────┘ └────────────┘
src └───────────────────┘ └────────────┘
typ └───────────────────┘ └────────────┘
748
749 def sum_prod_distrib (α β γ) [measurable_space α] [measurable_space β] [measurable_space γ] :
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
750 measurable_equiv ((α ⊕ β) × γ) ((α × γ) ⊕ (β × γ)) :=
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ ┴ ┴ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────────┘
751 { to_equiv := equiv.sum_prod_distrib α β γ,
id └────────────────────┘ ┴ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴
752 measurable_to_fun :=
753 begin
st └─────
754 refine measurable_of_measurable_union_cover
id └──────────────────────────────────┘
src └─────┘└──────────────────────────────────┘└
typ └─────┘└──────────────────────────────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ────────────────────────────────────────────────
755 ((range sum.inl).prod univ)
id └─────┘
src ─────┘ ┴└─────┘└─────┘ └─
typ ─────┘ ┴└─────┘└─────┘ └─
doc ─────┘ ┴ └─────┘ └─
txt ─────┘ ┴ └─────┘ └─
par ─────┘ ┴ └─────┘ └─
pid ─────┘ ┴ └─────┘ └─
st ──────────────────────────────────
756 ((range sum.inr).prod univ)
id └───┘ └─────┘ └──┘
src ─────┘ └───┘┴└─────┘└─────┘└──┘└─
typ ─────┘ └───┘┴└─────┘└─────┘└──┘└─
doc ─────┘ └───┘┴ └─────┘ └─
txt ─────┘ ┴ └─────┘ └─
par ─────┘ ┴ └─────┘ └─
pid ─────┘ ┴ └─────┘ └─
st ──────────────────────────────────
757 (is_measurable_set_prod is_measurable_range_inl is_measurable.univ)
id └─────────────────────┘
src ─────┘ ┴└─────────────────────┘┴ └─
typ ─────┘ ┴└─────────────────────┘┴ └─
doc ─────┘ ┴ ┴ └─
txt ─────┘ ┴ ┴ └─
par ─────┘ ┴ ┴ └─
pid ─────┘ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────────────
758 (is_measurable_set_prod is_measurable_range_inr is_measurable.univ)
id └────────────────────┘ └─────────────────────┘ └────────────────┘
src ─────┘ └────────────────────┘┴└─────────────────────┘┴└────────────────┘└─
typ ─────┘ └────────────────────┘┴└─────────────────────┘┴└────────────────┘└─
doc ─────┘ ┴ ┴ └─
txt ─────┘ ┴ ┴ └─
par ─────┘ ┴ ┴ └─
pid ─────┘ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────────────
759 (assume ⟨ab, c⟩ s, by cases ab; simp [set.prod_eq])
id └┘ └─────────┘
src ─────┘ └┘ └┘ └───┘ ┴└────┘ └┘└────┘└─────────┘┴└─
typ ─────┘ └┘ └┘ └───┘ ┴└────┘└┘└┘└────┘└─────────┘┴└─
doc ─────┘ └┘ └┘ └───┘ ┴└────┘ └┘└────┘ ┴└─
txt ─────┘ └┘ └┘ └───┘ ┴└────┘ └┘└────┘ ┴└─
par ─────┘ └┘ └┘ └───┘ ┴└────┘ └┘└────┘ ┴└─
pid ─────┘ └┘ └┘ └───┘ └─────┘ └──────┘ └──
st ──────────────────────────┘└───────────────────────────┘└─
760 _
src ────────
typ ────────
doc ────────
txt ────────
par ────────
pid ────────
st ────────
761 _,
src ──────┘
typ ──────┘
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘└─
762 { refine (set.prod (range sum.inl) univ).symm.measurable_coe_iff.1 _,
id └──────┘ └───┘ └─────┘ └──┘
src └─────┘ └──────┘┴ └───┘┴└─────┘└┘└──┘└───────────────────────────┘
typ └─────┘ └──────┘┴ └───┘┴└─────┘└┘└──┘└───────────────────────────┘
doc └─────┘ ┴ └───┘┴ └┘ └───────────────────────────┘
txt └─────┘ ┴ ┴ └┘ └───────────────────────────┘
par └─────┘ ┴ ┴ └┘ └───────────────────────────┘
pid ┴ ┴ ┴ └┘ └───────────────────────────┘
st ─────┘└────────────────────────────────────────────────────────────────┘└─
763 refine (prod_congr set.range_inl (set.univ _)).symm.measurable_coe_iff.1 _,
id └────────┘ └───────────┘ └──────┘
src └─────┘ └────────┘┴└───────────┘┴ └──────┘└──────────────────────────────┘
typ └─────┘ └────────┘┴└───────────┘┴ └──────┘└──────────────────────────────┘
doc └─────┘ ┴ ┴ └──────────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────────┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
764 dsimp [(∘)],
id ┴
src └─────┘┴└─┘
typ └─────┘┴└─┘
doc └─────┘ └─┘
txt └─────┘ └─┘
par └─────┘ └─┘
pid ┴┴ └─┘
st ────────────────┘└─
765 convert measurable_inl,
id └────────────┘
src └──────┘└────────────┘
typ └──────┘└────────────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ───────────────────────────┘└─
766 ext ⟨a, c⟩, refl },
src └────────┘ └───┘
typ └────────┘ └───┘
doc └────────┘ └───┘
txt └────────┘ └───┘
par └────────┘ └───┘
pid └─────┘ ┴
st ───────────────┘└─────┘└┘└
767 { refine (set.prod (range sum.inr) univ).symm.measurable_coe_iff.1 _,
id └──────┘ └───┘ └─────┘ └──┘
src └─────┘ └──────┘┴ └───┘┴└─────┘└┘└──┘└───────────────────────────┘
typ └─────┘ └──────┘┴ └───┘┴└─────┘└┘└──┘└───────────────────────────┘
doc └─────┘ ┴ └───┘┴ └┘ └───────────────────────────┘
txt └─────┘ ┴ ┴ └┘ └───────────────────────────┘
par └─────┘ ┴ ┴ └┘ └───────────────────────────┘
pid ┴ ┴ ┴ └┘ └───────────────────────────┘
st ───────────────────────────────────────────────────────────────────────┘└─
768 refine (prod_congr set.range_inr (set.univ _)).symm.measurable_coe_iff.1 _,
id └────────┘ └───────────┘ └──────┘
src └─────┘ └────────┘┴└───────────┘┴ └──────┘└──────────────────────────────┘
typ └─────┘ └────────┘┴└───────────┘┴ └──────┘└──────────────────────────────┘
doc └─────┘ ┴ ┴ └──────────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────────┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
769 dsimp [(∘)],
id ┴
src └─────┘┴└─┘
typ └─────┘┴└─┘
doc └─────┘ └─┘
txt └─────┘ └─┘
par └─────┘ └─┘
pid ┴┴ └─┘
st ────────────────┘└─
770 convert measurable_inr,
id └────────────┘
src └──────┘└────────────┘
typ └──────┘└────────────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ───────────────────────────┘└─
771 ext ⟨b, c⟩, refl }
src └────────┘ └───┘
typ └────────┘ └───┘
doc └────────┘ └───┘
txt └────────┘ └───┘
par └────────┘ └───┘
pid └─────┘ ┴
st ───────────────┘└─────┘└─
772 end,
st ────┘
773 measurable_inv_fun :=
774 begin
st └─────
775 refine measurable_sum _ _,
id └────────────┘
src └─────┘└────────────┘└──┘
typ └─────┘└────────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ──────────────────────────────┘└─
776 { convert measurable.prod_mk
id └────────────────┘
src └──────┘└────────────────┘└
typ └──────┘└────────────────┘└
doc └──────┘ └
txt └──────┘ └
par └──────┘ └
pid ┴ └
st ───────┘└──────────────────────────
777 (measurable_inl.comp (measurable.fst measurable_id)) (measurable.snd measurable_id),
id └─────────────────┘ └────────────┘ └────────────┘ └───────────┘
src ─────────┘ └─────────────────┘┴ └────────────┘┴ └─┘ └────────────┘┴└───────────┘┴
typ ─────────┘ └─────────────────┘┴ └────────────┘┴ └─┘ └────────────┘┴└───────────┘┴
doc ─────────┘ ┴ ┴ └─┘ ┴ ┴
txt ─────────┘ ┴ ┴ └─┘ ┴ ┴
par ─────────┘ ┴ ┴ └─┘ ┴ ┴
pid ─────────┘ ┴ ┴ └─┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
778 ext ⟨a, c⟩; refl },
src └────────┘ └───┘
typ └────────┘ └───┘
doc └────────┘ └───┘
txt └────────┘ └───┘
par └────────┘ └───┘
pid └─────┘ ┴
st ────────────────────────┘└┘└
779 { convert measurable.prod_mk
id └────────────────┘
src └──────┘└────────────────┘└
typ └──────┘└────────────────┘└
doc └──────┘ └
txt └──────┘ └
par └──────┘ └
pid ┴ └
st ───────────────────────────────────
780 (measurable_inr.comp (measurable.fst measurable_id)) (measurable.snd measurable_id),
id └─────────────────┘ └────────────┘ └────────────┘ └───────────┘
src ─────────┘ └─────────────────┘┴ └────────────┘┴ └─┘ └────────────┘┴└───────────┘┴
typ ─────────┘ └─────────────────┘┴ └────────────┘┴ └─┘ └────────────┘┴└───────────┘┴
doc ─────────┘ ┴ ┴ └─┘ ┴ ┴
txt ─────────┘ ┴ ┴ └─┘ ┴ ┴
par ─────────┘ ┴ ┴ └─┘ ┴ ┴
pid ─────────┘ ┴ ┴ └─┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
781 ext ⟨b, c⟩; refl }
src └────────┘ └───┘
typ └────────┘ └───┘
doc └────────┘ └───┘
txt └────────┘ └───┘
par └────────┘ └───┘
pid └─────┘ ┴
st ────────────────────────┘└─
782 end }
st ──────┘
783
784 def prod_sum_distrib (α β γ) [measurable_space α] [measurable_space β] [measurable_space γ] :
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
785 measurable_equiv (α × (β ⊕ γ)) ((α × β) ⊕ (α × γ)) :=
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ ┴ ┴ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────────┘
786 prod_comm.trans $ (sum_prod_distrib _ _ _).trans $ sum_congr prod_comm prod_comm
id └───────┘└────┘ └──────────────┘ └───┘ └───────┘ └───────┘ └───────┘
src └───────┘└────┘ └──────────────┘ └───┘ └───────┘ └───────┘ └───────┘
typ └───────┘└────┘ └──────────────┘ └───┘ └───────┘ └───────┘ └───────┘
787
788 def sum_prod_sum (α β γ δ)
789 [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] :
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
790 measurable_equiv ((α ⊕ β) × (γ ⊕ δ)) (((α × γ) ⊕ (α × δ)) ⊕ ((β × γ) ⊕ (β × δ))) :=
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────────┘
791 (sum_prod_distrib _ _ _).trans $ sum_congr (prod_sum_distrib _ _ _) (prod_sum_distrib _ _ _)
id └──────────────┘ └───┘ └───────┘ └──────────────┘ └──────────────┘
src └──────────────┘ └───┘ └───────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ └───┘ └───────┘ └──────────────┘ └──────────────┘
792
793 end measurable_equiv
794
795
796 namespace measurable_equiv
797
798 end measurable_equiv
799
800 namespace measurable_space
801
802 /-- Dynkin systems
803 The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras generated
804 by intersection stable set systems.
805 -/
806 structure dynkin_system (α : Type*) :=
id └───┘
typ └───┘
807 (has : set α → Prop)
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
808 (has_empty : has ∅)
id └─┘ ┴
src ┴
typ └─┘ ┴
809 (has_compl : ∀{a}, has a → has (-a))
id ┴┴ └─┘ ┴ └─┘ ┴┴
src ┴
typ ┴┴ └─┘ ┴ └─┘ ┴┴
810 (has_Union_nat : ∀{f:ℕ → set α}, pairwise (disjoint on f) → (∀i, has (f i)) → has (⋃i, f i))
id ┴ ┴ ┴ └─┘ ┴ └──────┘ └──────┘ └┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴┴┴ ┴ ┴
src ┴ └─┘ └──────┘ └──────┘ └┘ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ └──────┘ └──────┘ └┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴┴┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴
811
812 theorem Union_decode2_disjoint_on
813 {β} [encodable β] {f : β → set α} (hd : pairwise (disjoint on f)) :
id └───────┘ ┴ ┴ └─┘ ┴ └──────┘ └──────┘ └┘ ┴
src └───────┘ └─┘ └──────┘ └──────┘ └┘
typ └───────┘ ┴ ┴ └─┘ ┴ └──────┘ └──────┘ └┘ ┴
doc └───────┘ └──────┘ └──────┘
814 pairwise (disjoint on λ i, ⋃ b ∈ decode2 β i, f b) :=
id └──────┘ └──────┘ └┘ ┴ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴
src └──────┘ └──────┘ └┘ ┴ └─────┘ ┴
typ └──────┘ └──────┘ └┘ ┴ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴
815 begin
st └─────
816 rintro i j ij x ⟨h₁, h₂⟩,
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └────────────────┘
st ─────────────────────────┘└─
817 revert h₁ h₂,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ─────────────┘└─
818 simp, intros b₁ e₁ h₁ b₂ e₂ h₂,
src └──┘ └──────────────────────┘
typ └──┘ └──────────────────────┘
doc └──┘ └──────────────────────┘
txt └──┘ └──────────────────────┘
par └──┘ └──────────────────────┘
pid └────────────────┘
st ─────┘└────────────────────────┘└─
819 refine hd _ _ _ ⟨h₁, h₂⟩,
id └┘ └┘ └┘
src └─────┘ └─────┘ └┘ ┴
typ └─────┘└┘└─────┘ └┘└┘└┘┴
doc └─────┘ └─────┘ └┘ ┴
txt └─────┘ └─────┘ └┘ ┴
par └─────┘ └─────┘ └┘ ┴
pid ┴ └─────┘ └┘ ┴
st ─────────────────────────┘└─
820 cases encodable.mem_decode2.1 e₁,
id └───────────────────┘ └┘
src └────┘└───────────────────┘└─┘
typ └────┘└───────────────────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────────────────────────────────┘└─
821 cases encodable.mem_decode2.1 e₂,
id └───────────────────┘ └┘
src └────┘└───────────────────┘└─┘
typ └────┘└───────────────────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────────────────────────────────┘└─
822 exact mt (congr_arg _) ij
id └┘ └───────┘ └┘
src └────┘└┘┴ └───────┘└──┘ ┴
typ └────┘└┘┴ └───────┘└──┘└┘┴
doc └────┘ ┴ └──┘ ┴
txt └────┘ ┴ └──┘ ┴
par └────┘ ┴ └──┘ ┴
pid ┴ ┴ └──┘ ┴
st ───────────────────────────┘
823 end
st └─┘
824
825 namespace dynkin_system
826
827 @[ext] lemma ext :
doc └─┘
828 ∀{d₁ d₂ : dynkin_system α}, (∀s:set α, d₁.has s ↔ d₂.has s) → d₁ = d₂
id ┴ └───────────┘ ┴ ┴ └─┘ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴ └┘ ┴ └┘
src └───────────┘ └─┘ └──┘ ┴ └──┘ ┴
typ ┴ └───────────┘ ┴ ┴ └─┘ ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴ └┘ ┴ └┘
doc └───────────┘
829 | ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h :=
id └┘ └┘ ┴
typ └┘ └┘ ┴
830 have s₁ = s₂, from funext $ assume x, propext $ h x,
id ┴ └────┘ ┴ └─────┘ ┴
src ┴ └────┘ └─────┘
typ ┴ └────┘ ┴ └─────┘ ┴
831 by subst this
id └──┘
src └────┘ └
typ └────┘└──┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st └───────────
832
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
833 variable (d : dynkin_system α)
id └───────────┘
src └───────────┘
typ └───────────┘
doc └───────────┘
834
835 lemma has_compl_iff {a} : d.has (-a) ↔ d.has a :=
id ┴└──┘ ┴┴ ┴ ┴└──┘ ┴
src └──┘ ┴ ┴ └──┘
typ ┴└──┘ ┴┴ ┴ ┴└──┘ ┴
836 ⟨λ h, by simpa using d.has_compl h, λ h, d.has_compl h⟩
id ┴ └─────────┘ ┴ ┴ ┴└────────┘ ┴
src └──────────┘└─────────┘┴ └────────┘
typ ┴ └──────────┘└─────────┘┴┴ ┴ ┴└────────┘ ┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st └────────────────────────┘
837
838 lemma has_univ : d.has univ :=
id ┴└──┘ └──┘
src └──┘ └──┘
typ ┴└──┘ └──┘
839 by simpa using d.has_compl d.has_empty
id └─────────┘ └─────────┘
src └──────────┘└─────────┘┴└─────────┘└
typ └──────────┘└─────────┘┴└─────────┘└
doc └──────────┘ ┴ └
txt └──────────┘ ┴ └
par └──────────┘ ┴ └
pid ┴└────┘ ┴ └
st └────────────────────────────────────
840
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
841 theorem has_Union {β} [encodable β] {f : β → set α}
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
842 (hd : pairwise (disjoint on f)) (h : ∀i, d.has (f i)) : d.has (⋃i, f i) :=
id └──────┘ └──────┘ └┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴┴┴ ┴ ┴
src └──────┘ └──────┘ └┘ └──┘ └──┘ ┴ ┴
typ └──────┘ └──────┘ └┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴┴┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴
843 by rw encodable.Union_decode2; exact
id └─────────────────────┘
src └─┘└─────────────────────┘ └────┘
typ └─┘└─────────────────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └──────────────────────────────────
844 d.has_Union_nat (Union_decode2_disjoint_on hd)
id └─────────────┘ └───────────────────────┘ └┘
src └─────────────┘┴ └───────────────────────┘┴ └─
typ └─────────────┘┴ └───────────────────────┘┴└┘└─
doc ┴ ┴ └─
txt ┴ ┴ └─
par ┴ ┴ └─
pid ┴ ┴ └─
st ───────────────────────────────────────────────
845 (λ n, encodable.Union_decode2_cases d.has_empty h)
id └───────────────────────────┘ └─────────┘ ┴
src ─┘ └──┘└───────────────────────────┘┴└─────────┘┴ └─
typ ─┘ └──┘└───────────────────────────┘┴└─────────┘┴┴└─
doc ─┘ └──┘ ┴ ┴ └─
txt ─┘ └──┘ ┴ ┴ └─
par ─┘ └──┘ ┴ ┴ └─
pid ─┘ └──┘ ┴ ┴ ┴└
st ─────────────────────────────────────────────────────
846
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
847 theorem has_union {s₁ s₂ : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
848 (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₁ ∩ s₂ ⊆ ∅) : d.has (s₁ ∪ s₂) :=
id ┴└──┘ └┘ ┴└──┘ └┘ └┘ ┴ └┘ ┴ ┴ ┴└──┘ └┘ ┴ └┘
src └──┘ └──┘ ┴ ┴ ┴ └──┘ ┴
typ ┴└──┘ └┘ ┴└──┘ └┘ └┘ ┴ └┘ ┴ ┴ ┴└──┘ └┘ ┴ └┘
849 by rw union_eq_Union; exact
id └────────────┘
src └─┘└────────────┘ └────┘
typ └─┘└────────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └─────────────────────────
850 d.has_Union (pairwise_disjoint_on_bool.2 h)
id └─────────┘ └───────────────────────┘ ┴
src └─────────┘┴ └───────────────────────┘└─┘ └─
typ └─────────┘┴ └───────────────────────┘└─┘┴└─
doc ┴ └─┘ └─
txt ┴ └─┘ └─
par ┴ └─┘ └─
pid ┴ └─┘ └─
st ────────────────────────────────────────────
851 (bool.forall_bool.2 ⟨h₂, h₁⟩)
id └──────────────┘ └┘ └┘
src ─┘ └──────────────┘└─┘ └┘ └──
typ ─┘ └──────────────┘└─┘ └┘└┘└┘└──
doc ─┘ └─┘ └┘ └──
txt ─┘ └─┘ └┘ └──
par ─┘ └─┘ └┘ └──
pid ─┘ └─┘ └┘ └┘└
st ────────────────────────────────
852
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
853 lemma has_diff {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₂ ⊆ s₁) : d.has (s₁ \ s₂) :=
id └─┘ ┴ ┴└──┘ └┘ ┴└──┘ └┘ └┘ ┴ └┘ ┴└──┘ └┘ ┴ └┘
src └─┘ └──┘ └──┘ ┴ └──┘ ┴
typ └─┘ ┴ ┴└──┘ └┘ ┴└──┘ └┘ └┘ ┴ └┘ ┴└──┘ └┘ ┴ └┘
854 d.has_compl_iff.1 begin
id ┴└────────────┘┴
src └────────────┘┴
typ ┴└────────────┘┴
st └─────
855 simp [diff_eq, compl_inter],
id └─────┘ └─────────┘
src └────┘└─────┘└┘└─────────┘┴
typ └────┘└─────┘└┘└─────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────────────┘└─
856 exact d.has_union (d.has_compl h₁) h₂ (λ x ⟨h₁, h₂⟩, h₁ (h h₂)),
id └─────────┘ └─────────┘ └┘ └┘ └┘ └┘ ┴
src └────┘└─────────┘┴ └─────────┘┴ └┘ ┴ └──┘ └┘ └─┘ ┴ ┴ └┘
typ └────┘└─────────┘┴ └─────────┘┴└┘└┘└┘┴ └──┘└┘└┘└┘└─┘ ┴ ┴┴ └┘
doc └────┘ ┴ ┴ └┘ ┴ └──┘ └┘ └─┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘ ┴ └──┘ └┘ └─┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘ ┴ └──┘ └┘ └─┘ ┴ ┴ └┘
pid ┴ ┴ ┴ └┘ ┴ └──┘ └┘ └─┘ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────────┘└─
857 end
st ──┘
858
859 instance : partial_order (dynkin_system α) :=
id └───────────┘ └───────────┘ ┴
src └───────────┘ └───────────┘
typ └───────────┘ └───────────┘ ┴
doc └───────────┘
860 { le := λm₁ m₂, m₁.has ≤ m₂.has,
id ┴ └┘ └┘ └┘└──┘ ┴ └┘└──┘
src ┴ └──┘ ┴ └──┘
typ ┴ └┘ └┘ └┘└──┘ ┴ └┘└──┘
861 le_refl := assume a b, le_refl _,
id ┴ ┴ └─────┘
src └─────┘
typ ┴ ┴ └─────┘
862 le_trans := assume a b c, le_trans,
id ┴ ┴ ┴ └──────┘
src └──────┘
typ ┴ ┴ ┴ └──────┘
863 le_antisymm := assume a b h₁ h₂, ext $ assume s, ⟨h₁ s, h₂ s⟩ }
id ┴ ┴ └┘ └┘ └─┘ ┴ └┘ ┴ └┘ ┴
src └─┘
typ ┴ ┴ └┘ └┘ └─┘ ┴ └┘ ┴ └┘ ┴
864
865 def of_measurable_space (m : measurable_space α) : dynkin_system α :=
id └──────────────┘ ┴ └───────────┘ ┴
src └──────────────┘ └───────────┘
typ └──────────────┘ ┴ └───────────┘ ┴
doc └───────────┘
866 { has := m.is_measurable,
id ┴└────────────┘
src └────────────┘
typ ┴└────────────┘
867 has_empty := m.is_measurable_empty,
id ┴└──────────────────┘
src └──────────────────┘
typ ┴└──────────────────┘
868 has_compl := m.is_measurable_compl,
id ┴└──────────────────┘
src └──────────────────┘
typ ┴└──────────────────┘
869 has_Union_nat := assume f _ hf, m.is_measurable_Union f hf }
id ┴ ┴ └┘ ┴└──────────────────┘ ┴ └┘
src └──────────────────┘
typ ┴ ┴ └┘ ┴└──────────────────┘ ┴ └┘
870
871 lemma of_measurable_space_le_of_measurable_space_iff {m₁ m₂ : measurable_space α} :
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
872 of_measurable_space m₁ ≤ of_measurable_space m₂ ↔ m₁ ≤ m₂ :=
id └─────────────────┘ └┘ ┴ └─────────────────┘ └┘ ┴ └┘ ┴ └┘
src └─────────────────┘ ┴ └─────────────────┘ ┴ ┴
typ └─────────────────┘ └┘ ┴ └─────────────────┘ └┘ ┴ └┘ ┴ └┘
873 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
874
875 /-- The least Dynkin system containing a collection of basic sets. -/
876 inductive generate_has (s : set (set α)) : set α → Prop
id └─┘ └─┘ ┴ └─┘
src └─┘ └─┘ └─┘
typ └─┘ └─┘ ┴ └─┘
877 | basic : ∀t∈s, generate_has t
id ┴ ┴
typ ┴ ┴
878 | empty : generate_has ∅
id ┴
src ┴
typ ┴
879 | compl : ∀{a}, generate_has a → generate_has (-a)
id ┴ └──────────┘ ┴ ┴┴
src ┴
typ ┴ └──────────┘ ┴ ┴┴
880 | Union : ∀{f:ℕ → set α}, pairwise (disjoint on f) →
id ┴ ┴ └─┘ └──────┘ └──────┘ └┘ ┴
src ┴ └─┘ └──────┘ └──────┘ └┘
typ ┴ ┴ └─┘ └──────┘ └──────┘ └┘ ┴
doc └──────┘ └──────┘
881 (∀i, generate_has (f i)) → generate_has (⋃i, f i)
id ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴
882
883 def generate (s : set (set α)) : dynkin_system α :=
id └─┘ └─┘ ┴ └───────────┘ ┴
src └─┘ └─┘ └───────────┘
typ └─┘ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
884 { has := generate_has s,
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
885 has_empty := generate_has.empty s,
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
886 has_compl := assume a, generate_has.compl,
id ┴ └────────────────┘
src └────────────────┘
typ ┴ └────────────────┘
887 has_Union_nat := assume f, generate_has.Union }
id ┴ └────────────────┘
src └────────────────┘
typ ┴ └────────────────┘
888
889 instance : inhabited (dynkin_system α) := ⟨generate univ⟩
id └───────┘ └───────────┘ ┴ └──────┘ └──┘
src └───────┘ └───────────┘ └──────┘ └──┘
typ └───────┘ └───────────┘ ┴ └──────┘ └──┘
doc └───────────┘
890
891 def to_measurable_space (h_inter : ∀s₁ s₂, d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :=
id └┘ └┘ ┴└──┘ └┘ ┴└──┘ └┘ ┴└──┘ └┘ ┴ └┘
src └──┘ └──┘ └──┘ ┴
typ └┘ └┘ ┴└──┘ └┘ ┴└──┘ └┘ ┴└──┘ └┘ ┴ └┘
892 { measurable_space .
893 is_measurable := d.has,
id ┴└──┘
src └──┘
typ ┴└──┘
894 is_measurable_empty := d.has_empty,
id ┴└────────┘
src └────────┘
typ ┴└────────┘
895 is_measurable_compl := assume s h, d.has_compl h,
id ┴ ┴ ┴└────────┘ ┴
src └────────┘
typ ┴ ┴ ┴└────────┘ ┴
896 is_measurable_Union := assume f hf,
id ┴ └┘
typ ┴ └┘
897 have ∀n, d.has (disjointed f n),
id ┴ ┴└──┘ └────────┘ ┴ ┴
src └──┘ └────────┘
typ ┴ ┴└──┘ └────────┘ ┴ ┴
doc └────────┘
898 from assume n, disjointed_induct (hf n)
id ┴ └───────────────┘ └┘ ┴
src └───────────────┘
typ ┴ └───────────────┘ └┘ ┴
899 (assume t i h, h_inter _ _ h $ d.has_compl $ hf i),
id ┴ ┴ ┴ └─────┘ ┴ ┴└────────┘ └┘ ┴
src └────────┘
typ ┴ ┴ ┴ └─────┘ ┴ ┴└────────┘ └┘ ┴
900 have d.has (⋃n, disjointed f n), from d.has_Union disjoint_disjointed this,
id ┴└──┘ ┴┴┴ └────────┘ ┴ ┴ ┴└────────┘ └─────────────────┘ └──┘
src └──┘ ┴ ┴ └────────┘ └────────┘ └─────────────────┘
typ ┴└──┘ ┴┴┴ └────────┘ ┴ ┴ ┴└────────┘ └─────────────────┘ └──┘
doc ┴ ┴ └────────┘
901 by rwa [Union_disjointed] at this }
id └──────────────┘
src └───┘└──────────────┘└────────┘
typ └───┘└──────────────┘└────────┘
doc └───┘ └────────┘
txt └───┘ └────────┘
par └───┘ └────────┘
pid └┘ ┴└──────┘┴
st └────────────────────┘┴└───────┘
902
903 lemma of_measurable_space_to_measurable_space
904 (h_inter : ∀s₁ s₂, d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :
id └┘ └┘ ┴└──┘ └┘ ┴└──┘ └┘ ┴└──┘ └┘ ┴ └┘
src └──┘ └──┘ └──┘ ┴
typ └┘ └┘ ┴└──┘ └┘ ┴└──┘ └┘ ┴└──┘ └┘ ┴ └┘
905 of_measurable_space (d.to_measurable_space h_inter) = d :=
id └─────────────────┘ ┴└──────────────────┘ └─────┘ ┴ ┴
src └─────────────────┘ └──────────────────┘ ┴
typ └─────────────────┘ ┴└──────────────────┘ └─────┘ ┴ ┴
906 ext $ assume s, iff.rfl
id └─┘ ┴ └─────┘
src └─┘ └─────┘
typ └─┘ ┴ └─────┘
907
908 def restrict_on {s : set α} (h : d.has s) : dynkin_system α :=
id └─┘ ┴ ┴└──┘ ┴ └───────────┘ ┴
src └─┘ └──┘ └───────────┘
typ └─┘ ┴ ┴└──┘ ┴ └───────────┘ ┴
doc └───────────┘
909 { has := λt, d.has (t ∩ s),
id ┴ ┴└──┘ ┴ ┴ ┴
src └──┘ ┴
typ ┴ ┴└──┘ ┴ ┴ ┴
910 has_empty := by simp [d.has_empty],
src └────┘ ┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────┘
911 has_compl := assume t hts,
id ┴ └─┘
typ ┴ └─┘
912 have -t ∩ s = (- (t ∩ s)) \ -s,
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
913 from set.ext $ assume x, by by_cases x ∈ s; simp [h],
id └─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └───────┘ ┴┴┴ └────┘ ┴
typ └─────┘ ┴ └───────┘┴┴┴┴┴ └────┘┴┴
doc └───────┘ ┴ ┴ └────┘ ┴
txt └───────┘ ┴ ┴ └────┘ ┴
par └───────┘ ┴ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴┴ ┴
st └───────────────────────┘
914 by rw [this]; from d.has_diff (d.has_compl hts) (d.has_compl h)
id └──┘ └────────┘ └─┘ └─────────┘ ┴
src └──┘ ┴ └───┘└────────┘┴ ┴ └┘ └─────────┘┴ └─
typ └──┘└──┘┴ └───┘└────────┘┴ ┴└─┘└┘ └─────────┘┴┴└─
doc └──┘ ┴ └───┘ ┴ ┴ └┘ ┴ └─
txt └──┘ ┴ └───┘ ┴ ┴ └┘ ┴ └─
par └──┘ ┴ └───┘ ┴ ┴ └┘ ┴ └─
pid └┘ ┴ └───┘ ┴ ┴ └┘ ┴ └─
st └───────┘┴└───────────────────────────────────────────────────
915 (compl_subset_compl.mpr $ inter_subset_right _ _),
id └────────────────────┘ └────────────────┘
src ─────┘ └────────────────────┘┴ ┴└────────────────┘└───┘
typ ─────┘ └────────────────────┘┴ ┴└────────────────┘└───┘
doc ─────┘ ┴ ┴ └───┘
txt ─────┘ ┴ ┴ └───┘
par ─────┘ ┴ ┴ └───┘
pid ─────┘ ┴ ┴ └───┘
st ──────────────────────────────────────────────────────┘
916 has_Union_nat := assume f hd hf,
id ┴ └┘ └┘
typ ┴ └┘ └┘
917 begin
st └─────
918 rw [inter_comm, inter_Union],
id └────────┘ └─────────┘
src └──┘└────────┘└┘└─────────┘┴
typ └──┘└────────┘└┘└─────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────┘└───────────┘└──
919 apply d.has_Union_nat,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
920 { exact λ i j h x ⟨⟨_, h₁⟩, _, h₂⟩, hd i j h ⟨h₁, h₂⟩ },
id └┘ └┘ └┘
src └────┘ └────────┘ └─┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘
typ └────┘ └────────┘ └─┘└┘└────┘└┘└─┘└┘┴ ┴ ┴ ┴ └┘ └┘
doc └────┘ └────────┘ └─┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘
txt └────┘ └────────┘ └─┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘
par └────┘ └────────┘ └─┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘
pid ┴ └────────┘ └─┘ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴┴
st ───────┘└──────────────────────────────────────────────────┘└┘└
921 { simpa [inter_comm] using hf },
id └────────┘ └┘
src └─────┘└────────┘└──────┘ ┴
typ └─────┘└────────┘└──────┘└┘┴
doc └─────┘ └──────┘ ┴
txt └─────┘ └──────┘ ┴
par └─────┘ └──────┘ ┴
pid ┴┴ ┴┴└────┘ ┴
st ───────────────────────────────────┘└──
922 end }
st ──────┘
923
924 lemma generate_le {s : set (set α)} (h : ∀t∈s, d.has t) : generate s ≤ d :=
id └─┘ └─┘ ┴ ┴ ┴ ┴└──┘ ┴ └──────┘ ┴ ┴ ┴
src └─┘ └─┘ └──┘ └──────┘ ┴
typ └─┘ └─┘ ┴ ┴ ┴ ┴└──┘ ┴ └──────┘ ┴ ┴ ┴
925 λ t ht, ht.rec_on h d.has_empty
id ┴ └┘ └┘└─────┘ ┴ ┴└────────┘
src └─────┘ └────────┘
typ ┴ └┘ └┘└─────┘ ┴ ┴└────────┘
926 (assume a _ h, d.has_compl h)
id ┴ ┴ ┴ ┴└────────┘ ┴
src └────────┘
typ ┴ ┴ ┴ ┴└────────┘ ┴
927 (assume f hd _ hf, d.has_Union hd hf)
id ┴ └┘ ┴ └┘ ┴└────────┘ └┘ └┘
src └────────┘
typ ┴ └┘ ┴ └┘ ┴└────────┘ └┘ └┘
928
929 lemma generate_inter {s : set (set α)}
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
930 (hs : ∀t₁ t₂ : set α, t₁ ∈ s → t₂ ∈ s → (t₁ ∩ t₂).nonempty → t₁ ∩ t₂ ∈ s) {t₁ t₂ : set α}
id └─┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └──────┘ └┘ ┴ └┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘
typ └─┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └──────┘ └┘ ┴ └┘ ┴ ┴ └─┘ ┴
doc └──────┘
931 (ht₁ : (generate s).has t₁) (ht₂ : (generate s).has t₂) : (generate s).has (t₁ ∩ t₂) :=
id └──────┘ ┴ └─┘ └┘ └──────┘ ┴ └─┘ └┘ └──────┘ ┴ └─┘ └┘ ┴ └┘
src └──────┘ └─┘ └──────┘ └─┘ └──────┘ └─┘ ┴
typ └──────┘ ┴ └─┘ └┘ └──────┘ ┴ └─┘ └┘ └──────┘ ┴ └─┘ └┘ ┴ └┘
932 have generate s ≤ (generate s).restrict_on ht₂,
id └──────┘ ┴ ┴ └──────┘ ┴ └─────────┘ └─┘
src └──────┘ ┴ └──────┘ └─────────┘
typ └──────┘ ┴ ┴ └──────┘ ┴ └─────────┘ └─┘
933 from generate_le _ $ assume s₁ hs₁,
id └─────────┘ └┘ └─┘
src └─────────┘
typ └─────────┘ └┘ └─┘
934 have (generate s).has s₁, from generate_has.basic s₁ hs₁,
id └──────┘ ┴ └─┘ └┘ └────────────────┘ └┘ └─┘
src └──────┘ └─┘ └────────────────┘
typ └──────┘ ┴ └─┘ └┘ └────────────────┘ └┘ └─┘
935 have generate s ≤ (generate s).restrict_on this,
id └──────┘ ┴ ┴ └──────┘ ┴ └─────────┘ └──┘
src └──────┘ ┴ └──────┘ └─────────┘
typ └──────┘ ┴ ┴ └──────┘ ┴ └─────────┘ └──┘
936 from generate_le _ $ assume s₂ hs₂,
id └─────────┘ └┘ └─┘
src └─────────┘
typ └─────────┘ └┘ └─┘
937 show (generate s).has (s₂ ∩ s₁), from
id └──────┘ ┴ └─┘ └┘ ┴ └┘
src └──────┘ └─┘ ┴
typ └──────┘ ┴ └─┘ └┘ ┴ └┘
938 (s₂ ∩ s₁).eq_empty_or_nonempty.elim
id └┘ ┴ └┘ └──────────────────┘ └──┘
src ┴ └──────────────────┘ └──┘
typ └┘ ┴ └┘ └──────────────────┘ └──┘
939 (λ h, h.symm ▸ generate_has.empty _)
id ┴ ┴└───┘ ┴ └────────────────┘
src └───┘ ┴ └────────────────┘
typ ┴ ┴└───┘ ┴ └────────────────┘
940 (λ h, generate_has.basic _ (hs _ _ hs₂ hs₁ h)),
id ┴ └────────────────┘ └┘ └─┘ └─┘ ┴
src └────────────────┘
typ ┴ └────────────────┘ └┘ └─┘ └─┘ ┴
941 have (generate s).has (t₂ ∩ s₁), from this _ ht₂,
id └──────┘ ┴ └─┘ └┘ ┴ └┘ └──┘ └─┘
src └──────┘ └─┘ ┴
typ └──────┘ ┴ └─┘ └┘ ┴ └┘ └──┘ └─┘
942 show (generate s).has (s₁ ∩ t₂), by rwa [inter_comm],
id └──────┘ ┴ └─┘ └┘ ┴ └┘ └────────┘
src └──────┘ └─┘ ┴ └───┘└────────┘┴
typ └──────┘ ┴ └─┘ └┘ ┴ └┘ └───┘└────────┘┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └┘ ┴
st └──────────────┘┴
943 this _ ht₁
id └──┘ └─┘
typ └──┘ └─┘
944
945 lemma generate_from_eq {s : set (set α)}
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
946 (hs : ∀t₁ t₂ : set α, t₁ ∈ s → t₂ ∈ s → (t₁ ∩ t₂).nonempty → t₁ ∩ t₂ ∈ s) :
id └─┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └──────┘ └┘ ┴ └┘ ┴ ┴
src └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴
typ └─┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └──────┘ └┘ ┴ └┘ ┴ ┴
doc └──────┘
947 generate_from s = (generate s).to_measurable_space (assume t₁ t₂, generate_inter hs) :=
id └───────────┘ ┴ ┴ └──────┘ ┴ └─────────────────┘ └┘ └┘ └────────────┘ └┘
src └───────────┘ ┴ └──────┘ └─────────────────┘ └────────────┘
typ └───────────┘ ┴ ┴ └──────┘ ┴ └─────────────────┘ └┘ └┘ └────────────┘ └┘
doc └───────────┘
948 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
949 (generate_from_le $ assume t ht, generate_has.basic t ht)
id └──────────────┘ ┴ └┘ └────────────────┘ ┴ └┘
src └──────────────┘ └────────────────┘
typ └──────────────┘ ┴ └┘ └────────────────┘ ┴ └┘
950 (of_measurable_space_le_of_measurable_space_iff.mp $
id └────────────────────────────────────────────┘└─┘
src └────────────────────────────────────────────┘└─┘
typ └────────────────────────────────────────────┘└─┘
951 by rw [of_measurable_space_to_measurable_space];
id └─────────────────────────────────────┘
src └──┘└─────────────────────────────────────┘┴
typ └──┘└─────────────────────────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └──────────────────────────────────────────┘┴└─
952 from (generate_le _ $ assume t ht, is_measurable_generate_from ht))
id └─────────┘ └─────────────────────────┘
src └───┘ └─────────┘└─┘ ┴ └─────┘└─────────────────────────┘┴ ┴
typ └───┘ └─────────┘└─┘ ┴ └─────┘└─────────────────────────┘┴ ┴
doc └───┘ └─┘ ┴ └─────┘ ┴ ┴
txt └───┘ └─┘ ┴ └─────┘ ┴ ┴
par └───┘ └─┘ ┴ └─────┘ ┴ ┴
pid └───┘ └─┘ ┴ └─────┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────────┘
953
954 end dynkin_system
955
956 lemma induction_on_inter {C : set α → Prop} {s : set (set α)} {m : measurable_space α}
id └─┘ ┴ └─┘ └─┘ ┴ └──────────────┘ ┴
src └─┘ └─┘ └─┘ └──────────────┘
typ └─┘ ┴ └─┘ └─┘ ┴ └──────────────┘ ┴
957 (h_eq : m = generate_from s)
id ┴ ┴ └───────────┘ ┴
src ┴ └───────────┘
typ ┴ ┴ └───────────┘ ┴
doc └───────────┘
958 (h_inter : ∀t₁ t₂ : set α, t₁ ∈ s → t₂ ∈ s → (t₁ ∩ t₂).nonempty → t₁ ∩ t₂ ∈ s)
id └─┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └──────┘ └┘ ┴ └┘ ┴ ┴
src └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴
typ └─┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └──────┘ └┘ ┴ └┘ ┴ ┴
doc └──────┘
959 (h_empty : C ∅) (h_basic : ∀t∈s, C t) (h_compl : ∀t, m.is_measurable t → C t → C (- t))
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
960 (h_union : ∀f:ℕ → set α, (∀i j, i ≠ j → f i ∩ f j ⊆ ∅) →
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
961 (∀i, m.is_measurable (f i)) → (∀i, C (f i)) → C (⋃i, f i)) :
id ┴ ┴└────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src └────────────┘ ┴ ┴
typ ┴ ┴└────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴
962 ∀{t}, m.is_measurable t → C t :=
id ┴ ┴└────────────┘ ┴ ┴ ┴
src └────────────┘
typ ┴ ┴└────────────┘ ┴ ┴ ┴
963 have eq : m.is_measurable = dynkin_system.generate_has s,
id ┴└────────────┘ ┴ └────────────────────────┘ ┴
src └────────────┘ ┴ └────────────────────────┘
typ ┴└────────────┘ ┴ └────────────────────────┘ ┴
doc └────────────────────────┘
964 by rw [h_eq, dynkin_system.generate_from_eq h_inter]; refl,
id └──┘ └────────────────────────────┘ └─────┘
src └──┘ └┘└────────────────────────────┘┴ ┴ └──┘
typ └──┘└──┘└┘└────────────────────────────┘┴└─────┘┴ └──┘
doc └──┘ └┘ ┴ ┴ └──┘
txt └──┘ └┘ ┴ ┴ └──┘
par └──┘ └┘ ┴ ┴ └──┘
pid └┘ └┘ ┴ ┴
st └───────┘└──────────────────────────────────────┘┴└────┘
965 assume t ht,
id ┴ └┘
typ ┴ └┘
966 have dynkin_system.generate_has s t, by rwa [eq] at ht,
id └────────────────────────┘ ┴ ┴ └┘
src └────────────────────────┘ └───┘└┘└─────┘
typ └────────────────────────┘ ┴ ┴ └───┘└┘└─────┘
doc └────────────────────────┘ └───┘ └─────┘
txt └───┘ └─────┘
par └───┘ └─────┘
pid └┘ ┴└────┘
st └──────┘┴└────┘
967 this.rec_on h_basic h_empty
id └──┘└─────┘ └─────┘ └─────┘
src └─────┘
typ └──┘└─────┘ └─────┘ └─────┘
968 (assume t ht, h_compl t $ by rw [eq]; exact ht)
id ┴ └┘ └─────┘ ┴ └┘ └┘
src └──┘└┘┴ └────┘
typ ┴ └┘ └─────┘ ┴ └──┘└┘┴ └────┘└┘
doc └──┘ ┴ └────┘
txt └──┘ ┴ └────┘
par └──┘ ┴ └────┘
pid └┘ ┴ ┴
st └─────┘┴└────────┘
969 (assume f hf ht, h_union f hf $ assume i, by rw [eq]; exact ht _)
id ┴ └┘ └┘ └─────┘ ┴ └┘ ┴ └┘ └┘
src └──┘└┘┴ └────┘ └┘
typ ┴ └┘ └┘ └─────┘ ┴ └┘ ┴ └──┘└┘┴ └────┘└┘└┘
doc └──┘ ┴ └────┘ └┘
txt └──┘ ┴ └────┘ └┘
par └──┘ ┴ └────┘ └┘
pid └┘ ┴ ┴ └┘
st └─────┘┴└──────────┘
970
971 end measurable_space